Skip to content

Commit 3854104

Browse files
authored
Read definitional theorems ending in "_dict" (#49)
1 parent 833dbfe commit 3854104

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/exporter.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,7 +184,7 @@ object Exporter {
184184
* @define isace /span></code
185185
*/
186186
def is_eq_axiom(a:Entity[Axiom]): Option[(String,Term,List[Typ],Term)] = {
187-
if (!(a.name.endsWith("_def") || a.name.endsWith("_def_raw"))) None
187+
if (!(a.name.endsWith("_def") || a.name.endsWith("_def_raw") || a.name.endsWith("_dict"))) None
188188
else a.the_content.prop.term match {
189189
case App(App(Term.Const(id, _), _), _) if id != "Pure.eq" =>
190190
if (verbose) progress.echo("axiom " + a.name + ": cannot extract definition because it is headed by " + id + " instead of Pure.eq")

0 commit comments

Comments
 (0)