Email Gateway (Aug 22 2022 at 16:54): Email Gateway (Aug 22 2022 at 16:54):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I am having problems discharging the proof obligations for a nominal
function that I have written. The short sequence of 'apply's that I have
used in previous proofs, and have seen in uses of Nominal2 in the AFP, is
not working.
I notice the appearance of 'default' and 'invariant' on some nominal
functions in the AFP. I can see what the type signatures of these are and
can guess how to construct them.
My questions is: What are these used for and can they help?
Cheers
Mark
Last updated: Nov 21 2024 at 12:39 UTC