diff options
Diffstat (limited to 'coq/ex')
-rw-r--r-- | coq/ex/indent.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index c452cd1b..7218fa63 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -40,6 +40,12 @@ Proof. }} Qed. +Let x (* Precedence of "else" w.r.t "," and "->"! *) + : if true then nat * nat else nat -> + nat + := (if true then 1 else 2, + 3). + Module Y. Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. Proof with auto with arith. |