Bas Spitters (Nov 13 2020 at 12:22): Bas Spitters (Nov 13 2020 at 12:22):This example stopped working for me:
http://github.com/mattam82/Coq-Equations/raw/master/doc/equations_intro.v
Equations head {A} (l : list A) (pf : l <> nil) : A :=
head nil pf with (pf eq_refl) := { | x :=! x };
head (cons a v) _ := a.
Error: Illegal application (Non-functional construction):
The expression "!" of type "equations_tag" cannot be applied to the term
"x" : "False"
Matthieu Sozeau (Nov 13 2020 at 12:54):IIRC, the idiomatic way is now { | ! } instead of { | x :=! x }
Bas Spitters (Nov 13 2020 at 13:29):@Matthieu Sozeau Thanks. That works. Please consider updating the file.
Last updated: Apr 20 2024 at 02:40 UTC