Open mtzguido opened 1 month ago
I was looking at it today. We do send a query to typecheck the argument, and core checker successfully typechecks the term at type vprop. My guess is because of iota reduction. If we write it as if false then emp else 1
then it fails.
This works, despite the ill-typed if.