diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-23 17:29:54 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-23 17:29:54 +0200 |
| commit | 2202c8a405f50dcb589f69db106afcdbdd22cafd (patch) | |
| tree | ec9f90efb7c59e73d6fb0582caa2af708e2fa32d /coq/ex | |
| parent | afb29a670c537412d09cec703da7e8821c658196 (diff) | |
Fixing #183.
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 411347f0..1e9c17d8 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -91,6 +91,17 @@ Module Y. - induction x;simpl;intros... - induction x;simpl;intros... Qed. + Lemma L''' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x. + Proof using Type *. + intros x. + induction x;simpl;intros. + admit. + Admitted. + + Lemma L'''' : forall x:nat , 0 <= x. + Proof (fun x : nat => Nat.le_0_l x). + (* no indentation here since the proof above closes the proof. *) + Definition foo:nat := 0. End Y. Function div2 (n : nat) {struct n}: nat := @@ -314,7 +325,7 @@ Module TC. Next Obligation. Proof. - unfold pointwise_relation, all in * . + unfold pointwise_relation, all in *. intro. intros y H. intuition ; specialize (H x0) ; intuition. |