diff options
Diffstat (limited to 'test/golden/proofdefinefunction/glossing.golden')
| -rw-r--r-- | test/golden/proofdefinefunction/glossing.golden | 231 |
1 files changed, 0 insertions, 231 deletions
diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden deleted file mode 100644 index a638a71..0000000 --- a/test/golden/proofdefinefunction/glossing.golden +++ /dev/null @@ -1,231 +0,0 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( Marker "apply" ) - ( DefnOp - ( MixfixItem - ( TokenCons - ( Command "apply" ) - ( TokenCons InvisibleBraceL - ( HoleCons - ( TokenCons InvisibleBraceR - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ) - ) - ) - ( Marker "apply" ) NonAssoc - ) - [ NamedVar "f" - , NamedVar "x" - ] - ( TermVar - ( NamedVar "x" ) - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 8 - , locColumn = 1 - } - ) - ( Marker "dom" ) - ( DefnOp - ( MixfixItem - ( TokenCons - ( Command "dom" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) - ) - ) - ( Marker "dom" ) NonAssoc - ) - [ NamedVar "f" ] - ( TermVar - ( NamedVar "f" ) - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 13 - , locColumn = 1 - } - ) - ( Marker "rightunique" ) - ( DefnPredicate [] - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "right-unique" ) End - ) - ( Marker "rightunique" ) - ) - ) - ( NamedVar "f" :| [] ) - ( TermSymbol - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 14 - , locColumn = 31 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "f" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 18 - , locColumn = 1 - } - ) - ( Marker "relation" ) - ( DefnPredicate [] - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "relation" ) End - , pl = TokenCons - ( Word "relations" ) End - } - ) - ( Marker "relation" ) - ) - ) - ( NamedVar "f" :| [] ) - ( TermSymbol - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 19 - , locColumn = 29 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "f" ) - , TermVar - ( NamedVar "f" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 22 - , locColumn = 1 - } - ) - ( Marker "definefunctiontest" ) - ( Lemma [] - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 - , locColumn = 10 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 25 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 27 - , locColumn = 1 - } - ) - ( DefineFunction - ( Location - { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 26 - , locColumn = 5 - } - ) - ( NamedVar "f" ) - ( NamedVar "z" ) - ( TermVar - ( NamedVar "z" ) - ) - ( TermVar - ( NamedVar "x" ) - ) - ( Qed - { mloc = Nothing - , by = JustificationEmpty - } - ) - ) -]
\ No newline at end of file |