diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/output/Notations2.out | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/output/Notations2.out')
-rw-r--r-- | test-suite/output/Notations2.out | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ad60aecc..41d15937 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,10 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ x y : nat, -let b := 1 in -let c := b in -let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop @@ -32,11 +31,22 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | list1 => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| list1 => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat λ n : list(nat), match n with | nil => 2 @@ -84,3 +94,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α |