search

gdupont1 / rodin-hs

A collection of Haskell modules for handling Rodin files
GNU General Public License v3.0
0 stars 0 forks source link

Theory recursive definitions not showing in exported TeX #2

Closed gdupont1 closed 3 years ago

gdupont1 commented 3 years ago

When parsing a theory file, recursive definitions are absent; i.e.: if the operator is defined using a recursive definition, there is nothing below the signature and the well-definedness condition.

Also, no error is raised whatsoever.

gdupont1 commented 3 years ago

This is fixed now. It was due to a slight typo in the XML parser. Also, the printing of recursive definitions was inadequate (fixed as well).

(fixed in commit #b48d7332eaa18f645b8c18907cb2845da9d3768d)