Cab Dafny在match命令中使用导入的ADT

问题描述

嗨，我遇到了超时问题，并试图将我的文件分解为不同的模块，希望在处理导入了该模块的模块时，不必以VS代码重新验证一个经过验证的模块。如果有人知道这是否是避免超时的合理方法，我想听听。

但是我发现的更基本的问题是，一旦导入ADT，我就可以在if语句中使用in，但不能在match语句中使用。有关示例，请参见下面的代码。关于我在做什么错的任何想法吗？

module inner {
    datatype Twee = Node(value : int,left : Twee,right : Twee) | Leaf
    function rot(t:Twee) :Twee
  {
    match t 
       case Leaf => t 
       case Node(v,l,r) => Node(v,r,l)
  }
}
module outer {
import TL = inner 
function workingIf(t:TL.Twee) :TL.Twee
  { if (t == TL.Leaf) then TL.Leaf else t }  
function failingMatch(t:TL.Twee) :TL.Twee
  {
    match t 
       case TL.Leaf => t  // error "darrow expected"
       case TL.Node(v,r) => TL.Node(v,l)
 }  
}

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

adt dafny module module