diff options
author | qunyanm <unknown> | 2015-03-05 12:04:37 -0800 |
---|---|---|
committer | qunyanm <unknown> | 2015-03-05 12:04:37 -0800 |
commit | db30cafd94527e73e969457c9c00e8c67300d7d4 (patch) | |
tree | 304827ba0d57583141f110b2834ae040b7453bb4 /Test/hofs | |
parent | dbce023dbbbc2a73853c3d2b6251e85d4d627376 (diff) |
Stop pretty-print from emitting deprecated semi-colons.
Diffstat (limited to 'Test/hofs')
-rw-r--r-- | Test/hofs/Fold.dfy | 4 | ||||
-rw-r--r-- | Test/hofs/Monads.dfy | 8 | ||||
-rw-r--r-- | Test/hofs/TreeMapSimple.dfy | 4 |
3 files changed, 8 insertions, 8 deletions
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy index 50b5569b..6ca2d3b1 100644 --- a/Test/hofs/Fold.dfy +++ b/Test/hofs/Fold.dfy @@ -1,9 +1,9 @@ // RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -datatype List<A> = Nil | Cons(A,List<A>); +datatype List<A> = Nil | Cons(A,List<A>) -datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int); +datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int) function method Eval(e : Expr): int { diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy index a221f818..3598d2b3 100644 --- a/Test/hofs/Monads.dfy +++ b/Test/hofs/Monads.dfy @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t" abstract module Monad { - type M<A>; + type M<A> function method Return(x: A): M<A> function method Bind(m: M<A>, f:A -> M<B>):M<B> @@ -30,7 +30,7 @@ abstract module Monad { } module Identity refines Monad { - datatype M<A> = I(A); + datatype M<A> = I(A) function method Return<A>(x: A): M<A> { I(x) } @@ -62,7 +62,7 @@ module Identity refines Monad { } module Maybe refines Monad { - datatype M<A> = Just(A) | Nothing; + datatype M<A> = Just(A) | Nothing function method Return<A>(x: A): M<A> { Just(x) } @@ -96,7 +96,7 @@ module Maybe refines Monad { } module List refines Monad { - datatype M<A> = Cons(hd: A,tl: M<A>) | Nil; + datatype M<A> = Cons(hd: A,tl: M<A>) | Nil function method Return<A>(x: A): M<A> { Cons(x,Nil) } diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy index 3c70840e..a853b82c 100644 --- a/Test/hofs/TreeMapSimple.dfy +++ b/Test/hofs/TreeMapSimple.dfy @@ -1,9 +1,9 @@ // RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -datatype List<A> = Nil | Cons(head: A,tail: List<A>); +datatype List<A> = Nil | Cons(head: A,tail: List<A>) -datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>); +datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>) function ListData(xs : List) : set ensures forall x :: x in ListData(xs) ==> x < xs; |