diff options
Diffstat (limited to 'test/golden/byRef/glossing.golden')
| -rw-r--r-- | test/golden/byRef/glossing.golden | 245 |
1 files changed, 0 insertions, 245 deletions
diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden deleted file mode 100644 index 0af8bbb..0000000 --- a/test/golden/byRef/glossing.golden +++ /dev/null @@ -1,245 +0,0 @@ -[ BlockLemma - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "prop1" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 2 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "a" ) - , TermVar - ( NamedVar "a" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "prop2" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 6 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "b" ) - , TermVar - ( NamedVar "b" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( Marker "prop3" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 10 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "c" ) - , TermVar - ( NamedVar "c" ) - ] - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 12 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 14 - , locColumn = 1 - } - ) - ( Qed - { mloc = Just - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 13 - , locColumn = 5 - } - ) - , by = JustificationRef - ( Marker "prop1" :| [] ) - } - ) -, BlockLemma - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 16 - , locColumn = 1 - } - ) - ( Marker "prop4" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 17 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "e" ) - , TermVar - ( NamedVar "e" ) - ] - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 19 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 21 - , locColumn = 1 - } - ) - ( Have - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 20 - , locColumn = 5 - } - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 20 - , locColumn = 28 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "d" ) - ) - , TermVar - ( B - ( NamedVar "d" ) - ) - ] - ) - ) - ) - ( JustificationRef - ( Marker "prop1" :| [] ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 23 - , locColumn = 1 - } - ) - ( Marker "prop5" ) - ( Lemma [] - ( TermSymbol - ( Location - { locFile = "test/examples/byRef.tex" - , locLine = 24 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "f" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) -]
\ No newline at end of file |