diff options
author | Stefan Monnier <monnier@iro.umontreal.ca> | 2014-06-06 17:23:03 +0000 |
---|---|---|
committer | Stefan Monnier <monnier@iro.umontreal.ca> | 2014-06-06 17:23:03 +0000 |
commit | b9c06ced8e899854d06314b52d0182e123775afc (patch) | |
tree | 588fbaf256bcdcb8b8b7d889ed34538f8f7083f4 /coq/ex | |
parent | 1c0b0d32f95d7555943ab86a2de6666e39e84c13 (diff) |
* coq/coq-smie.el: Fix precedence of 'else'.
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. |