Overview  Index  Help 

PROOF_AST_UTILS

All Known Implementing Modules:

ProofAstUtilsProofCheckerFunTranslation


Utility function for the proof syntax.

           
Value summary

val mkNat : int -> ProofAst.term
           builds an unary natural number from an int.

val p : ProofAst.term -> ProofAst.term
           builds the predecessor of a term.

val s : ProofAst.term -> ProofAst.term
           builds the successor of a term.

val top : ProofAst.formula
          True type

 

       
Value detail

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).

 


Overview  Index  Help