Email Gateway (Aug 24 2022 at 22:20): Email Gateway (Aug 24 2022 at 22:20):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear All,
I believe we need more visual semantics when polymorphic types are
instantiated as the unit type.
Because sometimes it is confusing, especially when it is hidden behind
definition based on records or datatype.
I usually end up with the following, just because Isabelle decided to
instantiate everything as unit :
lemma ‹(λs. id s) = (λ_. ()) ›
by simp
lemma ‹inv (λs. id s) = (λ_. ()) ›
by force
lemma ‹(λs. id s) = inv(λ_. ()) ›
by force
lemma ‹inv (λs. id s) = inv(λ_. ()) ›
by force
While this example of lemmas are trivial, the same cases can be
hidden behind definitions based on a complicated data model, which is
sometimes hard to see(especially when reviewing Isabelle theories for some
paper).
Best wishes,
Yakoub.
Last updated: Apr 18 2024 at 08:19 UTC