diff options
| author | aarne <aarne@cs.chalmers.se> | 2005-12-20 22:38:38 +0000 |
|---|---|---|
| committer | aarne <aarne@cs.chalmers.se> | 2005-12-20 22:38:38 +0000 |
| commit | 59ee1bfd7c430576427943384f2e52efb9b3da08 (patch) | |
| tree | 7b737c9be67f41504649c376ab743987f2012d60 /examples/systemS | |
| parent | 7383e6d93ed111b418a27bb8605973fa77f3135c (diff) | |
full disjunctive patterns ; more prec levels for Exp
Diffstat (limited to 'examples/systemS')
| -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 |