diff options
author | 2017-09-25 10:49:18 +0200 | |
---|---|---|
committer | 2017-09-25 10:49:18 +0200 | |
commit | 43cd1660807b7da915d405d7aa9af8082b5d85f6 (patch) | |
tree | 6ed698aed58641eee9608a41b310e0bc7517c0b0 /test-suite | |
parent | f48ada1566daa5245244be3706c1b8c71237c374 (diff) | |
parent | 6d1b7368267a4da980980efa682cf3fb8f1e8394 (diff) |
Merge PR #1083: Fixing bug in building _rect scheme for inductive types with let-ins and non-recursively uniform parameters
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/Inductive.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index f746def5c..06f807f29 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -183,3 +183,20 @@ Module PolyNoLowerProp. Fail Check Foo True : Prop. End PolyNoLowerProp. + +(* Test building of elimination scheme with noth let-ins and + non-recursively uniform parameters *) + +Module NonRecLetIn. + + Unset Implicit Arguments. + + Inductive Ind (b:=2) (a:nat) (c:=1) : Type := + | Base : Ind a + | Rec : Ind (S a) -> Ind a. + + Check Ind_rect (fun n (b:Ind n) => b = b) + (fun n => eq_refl) + (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). + +End NonRecLetIn. |