ContentsIndex
SpecLanguage.PFormula
Synopsis
data PFormula
= Var Term
| Not PFormula
| And PFormula PFormula
| Forall Variable PFormula
type Term = String
toKFormula :: PFormula -> KFormula
pFormulaToIsabelle :: PFormula -> IO IsabelleFile
Documentation
data PFormula
First order formulae over Peano arithmetic
Constructors
Var Term
Not PFormula
And PFormula PFormula
Forall Variable PFormula
show/hide Instances
type Term = String
toKFormula :: PFormula -> KFormula

The instances for PFormula rely on instances for KFormula by defining a mapping PFormula -> KFormula

Another way would be to use some kind of generics.

pFormulaToIsabelle :: PFormula -> IO IsabelleFile
Produced by Haddock version 0.8