diff options
| author | Pierre Courtieu | 2019-05-24 13:08:01 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2019-06-17 18:06:13 +0200 |
| commit | cdc630c3d453fe0c1384e3faca268f9818828c26 (patch) | |
| tree | 0621b253644f1b2e50f27eaa05cef6eaf6192603 /coq/ex | |
| parent | 89a6166a2ee61ff9cc84ccffe681a275c64c6856 (diff) | |
fixing with inductive indentation.
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 32 |
1 files changed, 24 insertions, 8 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 1e9c17d8..43fcd9ac 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -11,27 +11,43 @@ Record a : Type := make_a { Module foo. Inductive test : nat -> Prop := - | C1 : forall n, test n + C1 : forall n, test n | C2 : forall n, test n | C3 : forall n, test n | C4 : forall n, test n. + + Inductive testbar' : nat -> Prop := + | Cbar1 : forall n, test n + | Cbar2 : forall n, test n + | Cbar3 : forall n, test n + | Cbar4 : forall n, test n. Inductive test2 : nat -> Prop - := C21 : forall n, test2 n - | C22 : forall n, test2 n - | C23 : forall n, test2 n - | C24 : forall n, test2 n. - + := | C21 : forall n, test2 n + | C22 : forall n, test2 n + | C23 : forall n, test2 n + | C24 : forall n, test2 n. + Inductive test' : nat -> Prop := - | C1' : forall n, test' n + C1' : forall n, test' n | C2' : forall n, test' n | C3' : forall n, test' n | C4' : forall n, test' n with - test2' : nat -> Prop := + test2' : nat -> Prop := + C21' : forall n, test2' n + | C22' : forall n, test2' n + | C23' : forall n, test2' n + | C24' : forall n, test2' n + with test3' : nat -> Prop := C21' : forall n, test2' n | C22' : forall n, test2' n | C23' : forall n, test2' n + | C24' : forall n, test2' n + with test4' : nat -> Prop := + | C21' : forall n, test2' n + | C22' : forall n, test2' n + | C23' : forall n, test2' n | C24' : forall n, test2' n. Let x := 1. Let y := 2. |