Overview  Index  Help 

CoreAstUtils


Utility function for the core syntax.

Opened structures

CoreAst

               
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 removeRegionCommand
           removes regions in commands abstract syntax.

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 removeRegionSequence
           removes regions in sequences abstract syntax.

val removeRegionValue
           removes regions in values 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).

removeRegionSequence

fun removeRegionSequence s

removes regions in sequences abstract syntax.

Parameters:
s
the sequence.
Returns:
the sequence without any region.

removeRegionCommand

fun removeRegionCommand c

removes regions in commands abstract syntax.

Parameters:
c
the expression.
Returns:
the command without any region.

removeRegionExpression

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

removes regions in expressions abstract syntax.

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

removeRegionValue

fun removeRegionValue v

removes regions in values abstract syntax.

Parameters:
v
the value.
Returns:
the value 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