Existential variable
Opened this issue · 0 comments
thyecust commented
Coq < Fixpoint remove (x: nat) (l: list nat): list nat :=
Coq < match l with
Coq < | [] => []
Coq < | h::t => if h=?x then t else h::remove x t
Coq < end.
Toplevel input, characters 91-93:
> | h::t => if h=?x then t else h::remove x t
> ^^
Error: Unknown existential variable.