blob: ae78a8e7141943fa7108749c28ad85515ad56100 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Inductive Foo(A : Type) : Prop :=
foo: A -> Foo A.
Arguments foo [A] _.
Scheme Foo_elim := Induction for Foo Sort Prop.
Goal forall (fn : Foo nat), { x: nat | foo x = fn }.
intro fn.
Fail induction fn as [n] using Foo_elim. (* should fail in a non-Prop context *)
Admitted.
|
