summaryrefslogtreecommitdiff
path: root/test/golden/calc/glossing.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/calc/glossing.golden')
-rw-r--r--test/golden/calc/glossing.golden574
1 files changed, 0 insertions, 574 deletions
diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden
deleted file mode 100644
index ccf40c4..0000000
--- a/test/golden/calc/glossing.golden
+++ /dev/null
@@ -1,574 +0,0 @@
-[ BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 1
- , locColumn = 1
- }
- )
- ( Marker "trivial" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 2
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "x" )
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 5
- , locColumn = 1
- }
- )
- ( Marker "irrelevant" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 6
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "z" )
- , TermVar
- ( NamedVar "z" )
- ]
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 9
- , locColumn = 1
- }
- )
- ( Marker "alsotrivial" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 10
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "y" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 12
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 20
- , locColumn = 1
- }
- )
- ( Calc
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 13
- , locColumn = 5
- }
- ) CalcUnquantified
- ( Equation
- ( TermVar
- ( NamedVar "y" )
- )
- (
- ( TermVar
- ( NamedVar "y" )
- , JustificationEmpty
- ) :|
- [
- ( TermVar
- ( NamedVar "y" )
- , JustificationRef
- ( Marker "trivial" :| [] )
- )
- ]
- )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 22
- , locColumn = 1
- }
- )
- ( Marker "trivial_biconditionals" )
- ( Lemma []
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 23
- , locColumn = 8
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "y" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 25
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 33
- , locColumn = 1
- }
- )
- ( Calc
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 26
- , locColumn = 5
- }
- ) CalcUnquantified
- ( Biconditionals
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 27
- , locColumn = 11
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "y" )
- , TermVar
- ( NamedVar "y" )
- ]
- )
- (
- ( PropositionalConstant IsTop
- , JustificationEmpty
- ) :|
- [
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 30
- , locColumn = 21
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "y" )
- , TermVar
- ( NamedVar "y" )
- ]
- , JustificationRef
- ( Marker "trivial" :| [] )
- )
- ]
- )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 35
- , locColumn = 1
- }
- )
- ( Marker "bounded_calc" )
- ( Lemma []
- ( Quantified Universally
- ( Scope
- ( Connected Implication
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 36
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 36
- , locColumn = 34
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- )
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 38
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 44
- , locColumn = 1
- }
- )
- ( Calc
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 39
- , locColumn = 5
- }
- )
- ( CalcForall
- ( NamedVar "x" :| [] )
- ( Just
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 39
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "A" )
- ]
- )
- )
- )
- ( Equation
- ( TermVar
- ( NamedVar "x" )
- )
- (
- ( TermVar
- ( NamedVar "x" )
- , JustificationEmpty
- ) :| []
- )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-, BlockLemma
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 46
- , locColumn = 1
- }
- )
- ( Marker "bounded_calc_such_that" )
- ( Lemma []
- ( Quantified Universally
- ( Scope
- ( Connected Implication
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 47
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( F
- ( TermVar
- ( NamedVar "A" )
- )
- )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 47
- , locColumn = 36
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 47
- , locColumn = 52
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( B
- ( NamedVar "x" )
- )
- , TermVar
- ( B
- ( NamedVar "x" )
- )
- ]
- )
- )
- )
- )
- )
-, BlockProof
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 49
- , locColumn = 1
- }
- )
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 55
- , locColumn = 1
- }
- )
- ( Calc
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 50
- , locColumn = 5
- }
- )
- ( CalcForall
- ( NamedVar "x" :| [] )
- ( Just
- ( Connected Conjunction
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 50
- , locColumn = 16
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Command "in" )
- ( ParameterArity 0 )
- ( Marker "elem" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "A" )
- ]
- )
- ( TermSymbol
- ( Location
- { locFile = "test/examples/calc.tex"
- , locLine = 50
- , locColumn = 36
- }
- )
- ( SymbolPredicate
- ( PredicateRelation
- ( RelationSymbol
- ( Symbol "=" )
- ( ParameterArity 0 )
- ( Marker "eq" )
- )
- )
- )
- [ TermVar
- ( NamedVar "x" )
- , TermVar
- ( NamedVar "x" )
- ]
- )
- )
- )
- )
- ( Equation
- ( TermVar
- ( NamedVar "x" )
- )
- (
- ( TermVar
- ( NamedVar "x" )
- , JustificationEmpty
- ) :| []
- )
- )
- ( Qed
- { mloc = Nothing
- , by = JustificationEmpty
- }
- )
- )
-] \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 09:50:22 +0000