ProofAstUtils
-
Utility function for the proof syntax.
-
top
val top : ProofAst.formula
-
True type
-
s
fun s t : ProofAst.term -> ProofAst.term
-
builds the successor of a term.
-
- Parameters:
-
-
t
-
the term.
- Returns:
-
the term s(t).
p
fun p t : ProofAst.term -> ProofAst.term
-
builds the predecessor of a term.
-
- Parameters:
-
-
t
-
the term.
- Returns:
-
the term p(t).
mkNat
fun mkNat n : int -> ProofAst.term
-
builds an unary natural number from an int.
-
- Parameters:
-
-
n
-
the integer value.
- Returns:
-
the unary natural number s^n(Z).