summaryrefslogtreecommitdiff
path: root/test/golden/prooffix/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/prooffix/glossing.golden')
-rw-r--r--test/golden/prooffix/glossing.golden98
1 files changed, 0 insertions, 98 deletions
diff --git a/test/golden/prooffix/glossing.golden b/test/golden/prooffix/glossing.golden
deleted file mode 100644
index 19af9d0..0000000
--- a/test/golden/prooffix/glossing.golden
+++ /dev/null
@@ -1,98 +0,0 @@
-[ BlockLemma
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "assumetest" )
- ( Lemma []
- ( Quantified Universally
- ( Scope
- ( TermSymbol
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 2
- , locColumn = 28
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 4
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 7
- , locColumn = 1
- }
- )
- ( Fix
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 5
- , locColumn = 5
- }
- )
- ( NamedVar "x" :| [] ) ( PropositionalConstant IsTop )
- ( Have
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 6
- , locColumn = 5
- }
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/prooffix.tex"
- , locLine = 6
- , locColumn = 13
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "x" )
- ]
- ) JustificationEmpty
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
- )
-] \ No newline at end of file