diff options
| author | dos-reis <gdr@axiomatics.org> | 2011-02-28 07:40:13 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2011-02-28 07:40:13 +0000 |
| commit | 26253eebb30fc5f6074836e387547d6353779049 (patch) | |
| tree | 3ffb4335f711110076f49a68704529fca25aad2c /src/algebra/boolean.spad.pamphlet | |
| parent | 78a4efb6f15ad686efe78fc10f3216719833d8aa (diff) | |
| download | open-axiom-26253eebb30fc5f6074836e387547d6353779049.tar.gz | |
* algebra/boolean.spad.pamphlet (PropositionalFormula):
Implement true and false. Fix thinko in notFormula.
Diffstat (limited to 'src/algebra/boolean.spad.pamphlet')
| -rw-r--r-- | src/algebra/boolean.spad.pamphlet | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet index 0b338604..1b5f5ce8 100644 --- a/src/algebra/boolean.spad.pamphlet +++ b/src/algebra/boolean.spad.pamphlet @@ -56,7 +56,7 @@ PropositionalLogic(): Category == Join(BooleanLogic,SetCategory) with )abbrev domain PROPFRML PropositionalFormula ++ Author: Gabriel Dos Reis ++ Date Created: Januray 14, 2008 -++ Date Last Modified: May 11, 2009 +++ Date Last Modified: February, 2011 ++ Description: This domain implements propositional formula build ++ over a term domain, that itself belongs to PropositionalLogic PropositionalFormula(T: SetCategory): Public == Private where @@ -101,9 +101,12 @@ PropositionalFormula(T: SetCategory): Public == Private where Rep == Union(T, Kernel %) import Kernel % import BasicOperator + import KernelFunctions2(Identifier,%) import List % -- Local names for proposition logical operators + macro FALSE == '%false + macro TRUE == '%true macro NOT == '%not macro AND == '%and macro OR == '%or @@ -120,6 +123,9 @@ PropositionalFormula(T: SetCategory): Public == Private where coerce(t: T): % == per t + false == per constantKernel FALSE + true == per constantKernel TRUE + not p == per kernel(operator(NOT, 1::Arity), [p], 1 + level p) @@ -232,7 +238,7 @@ PropositionalFormula(T: SetCategory): Public == Private where notFormula(p: %): OutputForm == case isNot p is - f@% => elt(outputForm 'not, [formula f])$OutputForm + f@% => elt(outputForm 'not, [notFormula f])$OutputForm otherwise => primaryFormula p andFormula(f: %): OutputForm == |