diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 11:27:49 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 11:27:49 +0000 |
| commit | ea043143aa90e0013bb8c4bd2ceb59217618f598 (patch) | |
| tree | a67d010c995649c15201504b3bcdb68521b8a0bd /coq/ex | |
| parent | 085f52535d2939e18cdd4ae5e6b24a2220465179 (diff) | |
Fixed small bugs in indentation.
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v new file mode 100644 index 00000000..b06ae922 --- /dev/null +++ b/coq/ex/indent.v @@ -0,0 +1,30 @@ +Require Import Arith. + + +Function div2 (n : nat) {struct n}: nat := + match n with + | 0 => 0 + | 1 => 0 + | S (S n') => S (div2 n') + end. + + +Module toto. + Lemma l1: forall n:nat, n = n. + toto. + Qed. + Lemma l2: forall n:nat, n = n. + toto. Qed. + Lemma l3: forall n:nat, n <= n. intro. Qed. + Lemma l4: forall n:nat, n <= n. Proof. intro. Qed. + Lemma l5 : forall n:nat, n <= n. + Proof. intro. + Qed. + Lemma l6: forall n:nat, n = n. + toto. + Lemma l7: forall n:nat, n = n. + toto. + Qed. + Qed. +End toto. + |