Databases
StackOverflow2013
Postsdbo
POFinding out the type signatures of a module/module type, in place
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POFinding out the type signatures of a module/module type, in place
    text
    copied!<p>This issue has been bugging me one too many times now. Is there a way to print the signature of each element of a module type in place in Coq.</p> <p>For instance:</p> <pre><code>Print Orders.OrderedType. Module Type Orders.OrderedType = Sig Parameter t Parameter eq Parameter eq_equiv Parameter lt Parameter lt_strorder Parameter lt_compat Parameter compare Parameter compare_spec Parameter eq_dec End </code></pre> <hr> <pre><code>Print Module Type Orders.OrderedType. Module Type Orders.OrderedType = Sig Parameter t Parameter eq Parameter eq_equiv Parameter lt Parameter lt_strorder Parameter lt_compat Parameter compare Parameter compare_spec Parameter eq_dec End </code></pre> <hr> <pre><code>About Orders.OrderedType. Module Type Coq.Structures.Orders.OrderedType </code></pre> <hr> <p>All of these are useless because they do not remind me of the type of each element...</p> <p>And I can't even use the error messages to remind me, since they are as stupid as:</p> <pre><code>Error: Signature components for label eq do not match. </code></pre> <p>Sure error message, do not tell me the expected type...</p> <p>I don't know whether this has been fixed in 8.4, but I'd really like a way to not have to look for where this has been defined in order to be reminded how it has been defined. Is there such a thing? :(</p> <hr> <p>Especially, finding out the definitions is just chasing along a <em>ridiculously</em> long chain of module combinations... Seriously:</p> <pre><code>Module Type OrderedType &lt;: DecidableType := DecStrOrder &lt;+ HasEqDec. </code></pre> <p>Yeah thanks...</p> <pre><code>Module Type DecStrOrder := StrOrder &lt;+ HasCompare. </code></pre> <p>Keep going...</p> <pre><code>Module Type StrOrder := EqualityType &lt;+ HasLt &lt;+ IsStrOrder. </code></pre> <p>...</p> <pre><code>Module Type EqualityType := Eq &lt;+ IsEq. </code></pre> <p>Sure...</p> <pre><code>Module Type Eq := Typ &lt;+ HasEq. </code></pre> <p>Ok...</p> <pre><code>Module Type Typ. Parameter Inline(10) t : Type. End Typ. </code></pre> <p>Finally, I know the type of <code>t</code>! \o/</p>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload