diff options
Diffstat (limited to 'test/golden/relation-notation')
| -rw-r--r-- | test/golden/relation-notation/encoding tasks.golden | 1 | ||||
| -rw-r--r-- | test/golden/relation-notation/generating tasks.golden | 61 | ||||
| -rw-r--r-- | test/golden/relation-notation/glossing.golden | 67 | ||||
| -rw-r--r-- | test/golden/relation-notation/parsing.golden | 47 | ||||
| -rw-r--r-- | test/golden/relation-notation/scanning.golden | 1 | ||||
| -rw-r--r-- | test/golden/relation-notation/tokenizing.golden | 24 | ||||
| -rw-r--r-- | test/golden/relation-notation/verification.golden | 1 |
7 files changed, 202 insertions, 0 deletions
diff --git a/test/golden/relation-notation/encoding tasks.golden b/test/golden/relation-notation/encoding tasks.golden new file mode 100644 index 0000000..0b26422 --- /dev/null +++ b/test/golden/relation-notation/encoding tasks.golden @@ -0,0 +1 @@ +fof(mathrel_notation_test,conjecture,elem(pair(fx,fy),fR)=>elem(pair(fx,fy),fR)).
\ No newline at end of file diff --git a/test/golden/relation-notation/generating tasks.golden b/test/golden/relation-notation/generating tasks.golden new file mode 100644 index 0000000..401b93f --- /dev/null +++ b/test/golden/relation-notation/generating tasks.golden @@ -0,0 +1,61 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = [] + , taskConjectureLabel = Marker "mathrel_notation_test" + , taskConjecture = Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + } +]
\ No newline at end of file diff --git a/test/golden/relation-notation/glossing.golden b/test/golden/relation-notation/glossing.golden new file mode 100644 index 0000000..4e4aa89 --- /dev/null +++ b/test/golden/relation-notation/glossing.golden @@ -0,0 +1,67 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/relation-notation.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "mathrel_notation_test" ) + ( Lemma [] + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + , TermVar + ( NamedVar "R" ) + ] + ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden new file mode 100644 index 0000000..33f2808 --- /dev/null +++ b/test/golden/relation-notation/parsing.golden @@ -0,0 +1,47 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/relation-notation.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "mathrel_notation_test" ) + ( Lemma [] + ( StmtConnected Implication + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationExpr + ( ExprVar + ( NamedVar "R" ) + ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationExpr + ( ExprVar + ( NamedVar "R" ) + ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/relation-notation/scanning.golden b/test/golden/relation-notation/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/relation-notation/scanning.golden @@ -0,0 +1 @@ +[]
\ No newline at end of file diff --git a/test/golden/relation-notation/tokenizing.golden b/test/golden/relation-notation/tokenizing.golden new file mode 100644 index 0000000..6799562 --- /dev/null +++ b/test/golden/relation-notation/tokenizing.golden @@ -0,0 +1,24 @@ +[ BeginEnv "proposition" +, Label "mathrel_notation_test" +, Word "if" +, BeginEnv "math" +, Variable "x" +, Command "mathrel" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Variable "y" +, EndEnv "math" +, Symbol "," +, Word "then" +, BeginEnv "math" +, Variable "x" +, Command "mathrel" +, InvisibleBraceL +, Variable "R" +, InvisibleBraceR +, Variable "y" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +]
\ No newline at end of file diff --git a/test/golden/relation-notation/verification.golden b/test/golden/relation-notation/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/relation-notation/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |