thyecust/coqwiki

Existential variable

Opened this issue · 0 comments

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.