Presentation given by @Théo Winterhalter
@Théo Winterhalter , I was a bit surprised that your external hint for the validity of
if _ then _ else _ did not talk about the condition. Does the condition have to be a variable? I guess it can't be an arbitrary program.
It seems to work as is for conditional of the form
if ek == ek' then ... else ...
(which we have in our examples)
Last updated: Feb 09 2023 at 03:06 UTC