CoreAstUtils
-
Utility function for the core 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).
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.