@zwarich Thanks, that's an interesting talk. The heavy use of opaque API lemmas is also something that feels like it should be done more with Coq/Lean-style ITPs. Leaning too heavily on definitional equality as a shortcut always felt wrong to me. One thing I appreciated about the simple Natural Number Game for Lean is that all the function definitions were sealed. People coming to ITPs from functional programming seem maybe too eager to rely on definitional equality.
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
=> View zwarich@hachyderm.io profile
text/geminiThis content has been proxied by September (3851b).