I'm getting the following surprising output from
Print Module — here
unlock is defined as
x = x but declared (by
x = 1. Wouldn't
x = 1 be more useful output?
Module x : xModuleType := Struct Definition body : nat. Definition unlock : x = x. End Module Type xModuleType = Sig Parameter body : nat. Parameter unlock : body = 1. End
Isn't the strangest here that the
x appearing in
unlock : x=x is not even declared?
Last updated: Oct 04 2023 at 22:01 UTC