Package | Description |
---|---|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
Modifier and Type | Field and Description |
---|---|
static Quantifier |
Quantifier.ALL
the usual 'forall' operator 'all' (be A a formula then
'all x.A' is true if and only if for all elements d of the
universe A{x<-d} (x substituted with d) is true
|
static Quantifier |
Quantifier.EX
the usual 'exists' operator 'ex' (be A a formula then
'ex x.A' is true if and only if there is at least one elements
d of the universe such that A{x<-d} (x substituted with d) is true
|
Copyright © 2003-2019 The KeY-Project.