Stream: Equations devs & users

Topic: Equations intro


view this post on Zulip 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"

view this post on Zulip Matthieu Sozeau (Nov 13 2020 at 12:54):

IIRC, the idiomatic way is now { | ! } instead of { | x :=! x }

view this post on Zulip Bas Spitters (Nov 13 2020 at 13:29):

@Matthieu Sozeau Thanks. That works. Please consider updating the file.


Last updated: Jan 29 2023 at 14:02 UTC