Stream: Coq users

Topic: `Print Module` using types from body instead of sealing

Paolo Giarrusso (Dec 19 2022 at 14:11):

I'm getting the following surprising output from Print Module — here unlock is defined as x = x but declared (by xModuleType) as 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

Pierre Courtieu (Dec 19 2022 at 14:21):

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