Overview  Index  Help 

CORE_AST_UTILS

All Known Implementing Modules:

CoreAstUtilsProofDerivPrettyPrinterProofInfer


Utility function for the core 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 removeRegionExpression : CoreAst.expression -> CoreAst.expression
           removes regions in expressions abstract syntax.

val removeRegionProgram : CoreAst.program -> CoreAst.program
           removes regions in programs abstract syntax.

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

removeRegionExpression

fun removeRegionExpression e : CoreAst.expression -> CoreAst.expression

removes regions in expressions abstract syntax.

Parameters:
e
the expression.
Returns:
the expression without any region.

removeRegionProgram

fun removeRegionProgram p : CoreAst.program -> CoreAst.program

removes regions in programs abstract syntax.

Parameters:
p
the program.
Returns:
the program without any region.

 


Overview  Index  Help