Skip to content
This repository has been archived by the owner on May 23, 2023. It is now read-only.

XML Export of a Spec with only definitions creates an empty module #1

Open
quicquid opened this issue Mar 31, 2016 · 0 comments
Open
Labels

Comments

@quicquid
Copy link
Contributor

Consider the module:

---- MODULE onlydefs ----

D(x,y) == x -+-> y
E(x) == ENABLED(x)
F(x,y) == x \cdot y

====

It is converted to an xml file containing no definitions:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<modules>
  <RootModule>onlydefs</RootModule>
  <context/>
  <ModuleNode>
    <location>
      <column>
        <begin>1</begin>
        <end>4</end>
      </column>
      <line>
        <begin>1</begin>
        <end>7</end>
      </line>
      <filename>onlydefs</filename>
    </location>
    <uniquename>onlydefs</uniquename>
  </ModuleNode>
</modules>

Mentioning a definition in a theorem makes it appear in the term database.

@quicquid quicquid self-assigned this Mar 31, 2016
@quicquid quicquid added the bug label Mar 31, 2016
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
Development

No branches or pull requests

1 participant