diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/systemS/ProofSymb.gf | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/examples/systemS/ProofSymb.gf b/examples/systemS/ProofSymb.gf index 4ff18ca14..3de1b91b7 100644 --- a/examples/systemS/ProofSymb.gf +++ b/examples/systemS/ProofSymb.gf @@ -18,7 +18,7 @@ concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in { RedAbs form = continue ["Reductio ad absurdum"] (task neg abs) where { neg = useTop (prefixR 4 "~" form) } ; - ExFalso form = finish (["Ex falso quodlibet"] ++ form.s) "Ø" ; --- form + ExFalso form = finish (["Ex falso quodlibet"] ++ toProve form) "Ø" ; --- form ConjSplit a b c = continue ["Conjunction split"] @@ -81,4 +81,10 @@ concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in { abs = "_|_" ; + toProve : PrecExp -> Str = \c -> + variants { + [] ; -- for generation + useTop c -- for parsing + } ; + }
\ No newline at end of file |