diff options
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. + |