6 lines
138 B
Text
6 lines
138 B
Text
|
example {A : Type} (f : A → A) (a : A) (H : f a = a) : unit :=
|
||
|
|
begin
|
||
|
|
induction H, -- this should raise an error
|
||
|
|
exact unit.star
|
||
|
|
end
|