diff options
Diffstat (limited to 'test/golden/prooffix')
| -rw-r--r-- | test/golden/prooffix/encoding tasks.golden | 4 | ||||
| -rw-r--r-- | test/golden/prooffix/generating tasks.golden | 48 | ||||
| -rw-r--r-- | test/golden/prooffix/glossing.golden | 55 | ||||
| -rw-r--r-- | test/golden/prooffix/parsing.golden | 56 | ||||
| -rw-r--r-- | test/golden/prooffix/scanning.golden | 1 | ||||
| -rw-r--r-- | test/golden/prooffix/tokenizing.golden | 31 | ||||
| -rw-r--r-- | test/golden/prooffix/verification.golden | 1 |
7 files changed, 196 insertions, 0 deletions
diff --git a/test/golden/prooffix/encoding tasks.golden b/test/golden/prooffix/encoding tasks.golden new file mode 100644 index 0000000..b92e552 --- /dev/null +++ b/test/golden/prooffix/encoding tasks.golden @@ -0,0 +1,4 @@ +fof(assumetest,conjecture,fx=fx). +------------------ +fof(assumetest,conjecture,fx=fx). +fof(assumetest1,axiom,fx=fx).
\ No newline at end of file diff --git a/test/golden/prooffix/generating tasks.golden b/test/golden/prooffix/generating tasks.golden new file mode 100644 index 0000000..7bba761 --- /dev/null +++ b/test/golden/prooffix/generating tasks.golden @@ -0,0 +1,48 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = [] + , taskConjectureLabel = Marker "assumetest" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "x" ) + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "assumetest1" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "x" ) + ] + ) + ] + , taskConjectureLabel = Marker "assumetest" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "x" ) + ] + } +]
\ No newline at end of file diff --git a/test/golden/prooffix/glossing.golden b/test/golden/prooffix/glossing.golden new file mode 100644 index 0000000..1b84ecc --- /dev/null +++ b/test/golden/prooffix/glossing.golden @@ -0,0 +1,55 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/prooffix.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetest" ) + ( Lemma [] + ( Quantified Universally + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "x" ) + ) + ] + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/prooffix.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( Fix + ( NamedVar "x" :| [] ) ( PropositionalConstant IsTop ) + ( Have + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "x" ) + ] + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/prooffix/parsing.golden b/test/golden/prooffix/parsing.golden new file mode 100644 index 0000000..26b2b35 --- /dev/null +++ b/test/golden/prooffix/parsing.golden @@ -0,0 +1,56 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/prooffix.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "assumetest" ) + ( Lemma [] + ( SymbolicQuantified Universally + ( NamedVar "x" :| [] ) Unbounded Nothing + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/prooffix.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( FixSymbolic + ( NamedVar "x" :| [] ) Unbounded + ( Have Nothing + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "x" ) :| [] + ) + ) + ) + ) JustificationEmpty ( Qed JustificationEmpty ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/prooffix/scanning.golden b/test/golden/prooffix/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/prooffix/scanning.golden @@ -0,0 +1 @@ +[]
\ No newline at end of file diff --git a/test/golden/prooffix/tokenizing.golden b/test/golden/prooffix/tokenizing.golden new file mode 100644 index 0000000..55064a0 --- /dev/null +++ b/test/golden/prooffix/tokenizing.golden @@ -0,0 +1,31 @@ +[ BeginEnv "proposition" +, Label "assumetest" +, Word "for" +, Word "all" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, Word "fix" +, BeginEnv "math" +, Variable "x" +, EndEnv "math" +, Symbol "." +, Word "then" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "x" +, EndEnv "math" +, Symbol "." +, EndEnv "proof" +]
\ No newline at end of file diff --git a/test/golden/prooffix/verification.golden b/test/golden/prooffix/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/prooffix/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |