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