blob: 599e8391ac93d4667edf4063b0c45b38efa159c9 (
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.
|
