A B C D E F G I J K L M N O P R S T U V W Y Z Other
A
- Abs - Constructor in FunAst
-
Abstraction: fn (x1 : f1, ..., xp : fp) => t.
- Actions - structure Parser.Actions
-
- add - Value in LIST_ASSOC
-
adds a new association, ensuring that only one association has this key.
- add - Value in ListAssoc
-
adds a new association, ensuring that only one association has this key.
- addAll - Value in LIST_ASSOC
-
adds a list of new association, ensuring that only one association has the added keys.
- addAll - Value in ListAssoc
-
adds a list of new association, ensuring that only one association has the added keys.
- addS - Value in SyntaxLexFun.UserDeclarations
-
- Affect - Constructor in ProofAst
-
assignment: x : tau := e.
- alpha - Value in TERMS
-
gives a new fresh variable with the given identifier.
- alpha - Value in Terms
-
gives a new fresh variable with the given identifier.
- alphaConvProc - Value in TERMS
-
converts the proc types in order to have the same bound variables.
- alphaConvProc - Value in Terms
-
converts the proc types in order to have the same bound variables.
- alphaEqual - Value in TERMS
-
check the equality of a pair of formulas up to alpha-equivalence.
- alphaEqual - Value in Terms
-
check the equality of a pair of formulas up to alpha-equivalence.
- alphaEqual - Value in FunTypeChecker
-
- App - Constructor in FunAst
-
Application: (t[a1, ..., an] u) as universal instantiation.
- append_last - Value in FunPrettyPrinter
-
appends a string at the end of the last string of a string list.
- areAllIn - Value in LIST_ASSOC
-
test if the first association list is a sub-list (without ordering consideration)
of the second list.
- areAllIn - Value in ListAssoc
-
test if the first association list is a sub-list (without ordering consideration)
of the second list.
- arg - Type in SyntaxLexFun.UserDeclarations
-
- assoc - Value in LIST_ASSOC
-
test if an association belongs to the association list.
- assoc - Value in ListAssoc
-
return the associated value of a key, or NONE.
B
- BasePrettyPrinter - structure BasePrettyPrinter
-
The First-Order LoopW Proof Checker base pretty-printer.
- BASE_PRETTY_PRINTER - signature BASE_PRETTY_PRINTER
-
The First-Order LoopW Proof Checker base pretty-printer.
- Block - Constructor in ProofAst
-
block: { s }{i}x:tau
- block - Type in ProofAst
-
blocks { s |> {i'}x':tau' }{i}x:tau.
- blockComment - Value in Parser
-
C
- Callcc - Constructor in FunAst
-
Catch operator: call/cc (fn k => t).
- checkClosedProg - Value in PROOF_CHECKER
-
check that the given program represents a correct proof.
- checkClosedProg - Value in ProofChecker
-
check that the given program represents a correct proof.
- checkExp - Value in ProofChecker
-
check that the given expression represents a correct proof.
- checkInSequence - Value in ProofChecker
-
- checkSequence - Value in ProofChecker
-
check that the given sequence represents a correct proof.
- checkValue - Value in ProofChecker
-
check that the given value represents a correct proof.
- Comm - Constructor in ProofAst
-
composed command: c; s.
- command - Datatype in ProofAst
-
commands.
- COMMENT1 - Value in SyntaxLexFun.Internal.StartStates
-
- COMMENT2 - Value in SyntaxLexFun.Internal.StartStates
-
- CommRegion - Constructor in ProofAst
-
- compile - Value in COMPILER
-
performs type inference and on-demand functional translation.
- compile - Value in Compiler
-
performs type checking and on-demand functional translation.
- COMPILER - signature COMPILER
-
The First-Order LoopW Proof Checker compiler.
- Compiler - structure Compiler
-
The First-Order LoopW Proof Checker compiler.
- compilerParams - Type in COMPILER
-
The type of compiling parameters.
- compilerParams - Type in Compiler
-
The type of compiling parameters.
- compVersion - Value in Main
-
Current compiler version number.
- convert - Value in SyntaxLexFun.UserDeclarations
-
- Cst - Constructor in ProofAst
-
constant declaration: cst x : tau = e; s.
- current - Value in SyntaxLexFun.UserDeclarations
-
- curstring - Value in SyntaxLexFun.UserDeclarations
-
D
- Dec - Constructor in ProofAst
-
decrementation: dec(x : tau).
- depth - Value in SyntaxLexFun.UserDeclarations
-
- display - Value in Error
-
converts a region into a string.
- dom - Value in PROOF_ENVIRONMENT
-
returns the domain of the environment.
- dom - Value in ProofEnvironment
-
returns the domain of the environment.
- doubleQuote - Value in PrettyPrinterKeywords
-
" value.
E
- EC - structure Parser.EC
-
- Empty - Constructor in ProofAst
-
empty sequence : [n/j] "substitution used for existential introduction".
- empty - Value in PROOF_ENVIRONMENT
-
the empty environment.
- empty - Value in ProofEnvironment
-
the empty environment.
- enterC - Value in SyntaxLexFun.UserDeclarations
-
- env - Type in PROOF_ENVIRONMENT
-
the typing environment.
- env - Type in ProofEnvironment
-
the typing environment.
- envEquals - Value in PROOF_ENVIRONMENT
-
test if the enviroment are equals.
- envEquals - Value in ProofEnvironment
-
test if the enviroment are equals.
- eof - Value in SyntaxLexFun.UserDeclarations
-
- Error - structure Error
-
The First-Order LoopW Proof Checker syntax error module.
- error - Value in Parser
-
- ESubst - Constructor in ProofAst
-
expression substitution: e :> {i/tau[i]} [e' : (n = m)].
- existsAllKey - Value in LIST_ASSOC
-
test if all the keys occurs in the association list.
- existsAllKey - Value in ListAssoc
-
test if all the keys occurs in the association list.
- ExpRegion - Constructor in ProofAst
-
- expression - Type in ProofAst
-
typed expressions e : tau.
- expType - Datatype in FunAst
-
first-order formulas.
F
- fail - Value in Error
-
displays the error message and region, and raise a failure.
- failm - Value in Error
-
displays the error message, and raise a failure.
- FFun - Constructor in ProofAst
-
n-ary function (s and p will be instances of this): f(tl)
- FId - Constructor in ProofAst
-
identifier.
- filterKey - Value in LIST_ASSOC
-
returns all the elements of the association for which the key belongs to
the given key list.
- filterKey - Value in ListAssoc
-
returns all the elements of the association for which the key belongs to
the given key list.
- For - Constructor in ProofAst
-
for-loop: for I : nat(i) := e : tau { s }{j}x:tau[i].
- formula - Datatype in ProofAst
-
first-order formulas.
- freeVars - Value in FunTypeChecker
-
- FunAst - structure FunAst
-
The First-Order LoopW Proof Checker functional programs abstract syntax.
- FunPrettyPrinter - structure FunPrettyPrinter
-
The First-Order LoopW Proof Checker functional pretty-printer.
- FunTranslation - structure FunTranslation
-
The First-Order LoopW Proof Checker translator into functional syntax.
- FunTypeChecker - structure FunTypeChecker
-
- FUN_PRETTY_PRINTER - signature FUN_PRETTY_PRINTER
-
The First-Order LoopW Proof Checker functional pretty-printer.
- FUN_TRANSLATION - signature FUN_TRANSLATION
-
The First-Order LoopW Proof Checker translator into functional syntax.
- fv_formula - Value in Terms
-
calculates the free variables of a formula.
- fv_formulas - Value in TERMS
-
calculates the free variables of a formula list.
- fv_formulas - Value in Terms
-
calculates the free variables of a formula list.
- fv_term - Value in TERMS
-
calculates the free variables of a term.
- fv_term - Value in Terms
-
calculates the free variables of a term.
- FZero - Constructor in ProofAst
-
zero: Z
G
- getKeyList - Value in LIST_ASSOC
-
returns the list of keys.
- getKeyList - Value in ListAssoc
-
returns the list of keys.
- getNat - Value in BasePrettyPrinter
-
converts a term into an integer if it is an unary natural number into an integer, returning NONE if not.
- getS - Value in SyntaxLexFun.UserDeclarations
-
- getValueList - Value in LIST_ASSOC
-
returns the list of values.
- getValueList - Value in ListAssoc
-
returns the list of values.
- getVarType - Value in PROOF_ENVIRONMENT
-
returns the type of an identifier in an environment.
- getVarType - Value in ProofEnvironment
-
returns the type of an identifier in an environment.
I
- Id - Constructor in ProofAst
-
identifier.
- Id - Constructor in FunAst
-
identifier.
- ident - Type in ProofAst
-
identifiers as string (numeroted for alpha-conversion).
- ident - Type in FunAst
-
identifiers as string (numeroted for alpha-conversion).
- idToken - Value in SyntaxLexFun.UserDeclarations
-
- img - Value in PROOF_ENVIRONMENT
-
returns the image of the environment.
- img - Value in ProofEnvironment
-
returns the image of the environment.
- Inc - Constructor in ProofAst
-
incrementation: inc(x : tau).
- init - Value in FunPrettyPrinter
-
- INITIAL - Value in SyntaxLexFun.Internal.StartStates
-
- initLexer - Value in SyntaxLexFun.UserDeclarations
-
- instring - Value in SyntaxLexFun.UserDeclarations
-
- Int - Constructor in ProofAst
-
natural number: n.
- Internal - structure SyntaxLexFun.Internal
-
- isAssoc - Value in ListAssoc
-
test if an association belongs to the association list.
- i_expression - Datatype in ProofAst
-
untyped expressions.
- i_sequence - Datatype in ProofAst
-
untyped sequences.
- i_value - Datatype in ProofAst
-
untyped values.
J
- Jump - Constructor in ProofAst
-
jump to a label: jump(k : ~tau [subst], etl)x:tau.
K
- keywords - Value in Parser
-
- kwd - Value in PRETTY_PRINTER_KEYWORDS
-
default keyword.
- kwd - Value in PrettyPrinterKeywords
-
default keyword.
- kwdAnd - Value in PRETTY_PRINTER_KEYWORDS
-
and keyword.
- kwdAnd - Value in PrettyPrinterKeywords
-
and keyword.
- kwdBot - Value in PRETTY_PRINTER_KEYWORDS
-
bot keyword.
- kwdBot - Value in PrettyPrinterKeywords
-
bot keyword.
- kwdExists - Value in PRETTY_PRINTER_KEYWORDS
-
exists keyword.
- kwdExists - Value in PrettyPrinterKeywords
-
exists keyword.
- kwdForall - Value in PRETTY_PRINTER_KEYWORDS
-
forall keyword.
- kwdForall - Value in PrettyPrinterKeywords
-
forall keyword.
- kwdImplies - Value in PRETTY_PRINTER_KEYWORDS
-
implies keyword.
- kwdImplies - Value in PrettyPrinterKeywords
-
implies keyword.
- kwdNeg - Value in PRETTY_PRINTER_KEYWORDS
-
neg keyword.
- kwdNeg - Value in PrettyPrinterKeywords
-
neg keyword.
- kwdStar - Value in PRETTY_PRINTER_KEYWORDS
-
star keyword.
- kwdStar - Value in PrettyPrinterKeywords
-
star keyword.
- kwdTop - Value in PRETTY_PRINTER_KEYWORDS
-
top keyword.
- kwdTop - Value in PrettyPrinterKeywords
-
top keyword.
- kwdVBar - Value in PRETTY_PRINTER_KEYWORDS
-
| keyword.
- kwdVBar - Value in PrettyPrinterKeywords
-
| keyword.
- kwdVdash - Value in PRETTY_PRINTER_KEYWORDS
-
|- keyword.
- kwdVdash - Value in PrettyPrinterKeywords
-
|- keyword.
L
- Label - Constructor in ProofAst
-
label definition: k : {i}~tau :{ s }{i}x:tau.
- leaveC - Value in SyntaxLexFun.UserDeclarations
-
- Lemma - Constructor in ProofAst
-
lemma (equation over term in a context): G |- n = m.
- Lemma - Constructor in FunAst
-
Lemma: f1, ..., fn |- f
- LetIn - Constructor in FunAst
-
Let binding: let (x1 : f1 = u1, ..., xp : fp = up) in t (as existential elimination).
- lexarg - Type in SyntaxLexFun.UserDeclarations
-
- LexerError - Exception in SyntaxLexFun.Internal
-
- LexError - Exception in SyntaxLexFun
-
- lexerror - Value in Parser
-
- lexresult - Type in SyntaxLexFun.UserDeclarations
-
- line - Value in SyntaxLexFun.UserDeclarations
-
- lineComment - Value in Parser
-
- linePos - Value in SyntaxLexFun.UserDeclarations
-
- ListAssoc - structure ListAssoc
-
Utility functions that deals with association lists.
- listConcatWith - Value in UTILS
-
flattens a list of list, inserting a separator between each inner lists.
- listConcatWith - Value in Utils
-
flattens a list of list, inserting a separator between each inner lists.
- listEquals - Value in UTILS
-
check if the two lists contains the same elements (not considering their
position in the list).
- listEquals - Value in Utils
-
check if the two lists contains the same elements (not considering their
position in the list).
- listFusion - Value in UTILS
-
merges the two list without duplicating identical elements.
- listFusion - Value in Utils
-
merges the two list without duplicating identical elements.
- listFusionPair - Value in UTILS
-
merges the two list without duplicating identical elements.
- listFusionPair - Value in Utils
-
merges the two list without duplicating identical elements.
- listMember - Value in UTILS
-
check if the given element belongs to the list.
- listMember - Value in Utils
-
check if the given element belongs to the list.
- listMemberRemove - Value in UTILS
-
check if the given element belongs to the list, and removes it.
- listMemberRemove - Value in Utils
-
check if the given element belongs to the list, and removes it.
- LIST_ASSOC - signature LIST_ASSOC
-
Utility functions that deals with association lists.
- locate - Value in SyntaxLexFun.UserDeclarations
-
- locate' - Value in SyntaxLexFun.UserDeclarations
-
M
- main - Value in Main
-
calls run() and wait for any exception in order to display the exception message.
- Main - structure Main
-
The First-Order LoopW Proof Checker main program.
- makeLexer - Value in SyntaxLexFun
-
- math - Value in PrettyPrinterKeywords
-
used to encapsulate tex-math string into $.
- mem - Value in FunTypeChecker
-
- memberKey - Value in LIST_ASSOC
-
test if a key belongs to the association list.
- memberKey - Value in ListAssoc
-
test if a key belongs to the association list.
- mkNat - Value in PROOF_AST_UTILS
-
builds an unary natural number from an int.
- mkNat - Value in ProofAstUtils
-
builds an unary natural number from an int.
- mkTuple - Value in FunTranslation
-
builds a typed singleton tuple from a term and a type.
N
- N - Constructor in SyntaxLexFun.Internal
-
- newline - Value in SyntaxLexFun.UserDeclarations
-
- newS - Value in SyntaxLexFun.UserDeclarations
-
- next - Value in FunPrettyPrinter
-
O
- omega2tuple - Value in FunTranslation
-
translates an imperative sequence type into a function tuple type.
- optFail - Value in Error
-
calls either fail or failm depending on the region Option.
- order - Value in FunTranslation
-
orders an environment according to a given variable list.
- orderSubst - Value in FunTranslation
-
orders a substitution according to a given variable list.
P
- p - Value in PROOF_AST_UTILS
-
builds the predecessor of a term.
- p - Value in ProofAstUtils
-
builds the predecessor of a term.
- p - Value in FunTypeChecker
-
- parseArgs - Value in Main
-
parses the argument list to build the tuple of options.
- parseFile - Value in Parser
-
- Parser - structure Parser
-
- parseStream - Value in Parser
-
- parseString - Value in Parser
-
- partitionWithKeyList - Value in LIST_ASSOC
-
partitions an association list in two list, according to the keys bonlonging to
the given key list.
- partitionWithKeyList - Value in ListAssoc
-
partitions an association list in two list, according to the keys bonlonging to
the given key list.
- pos - Type in SyntaxLexFun.UserDeclarations
-
- Pred - Constructor in FunAst
-
Pred function.
- PrettyPrinterKeywords - structure PrettyPrinterKeywords
-
The First-Order LoopW Proof Checker pretty-printer keywords for abstract syntax.
- PRETTY_PRINTER_KEYWORDS - signature PRETTY_PRINTER_KEYWORDS
-
The First-Order LoopW Proof Checker pretty-printer keywords for abstract syntax.
- printParams - Value in Compiler
-
prints the compiling parameters values.
- print_verb - Value in Compiler
-
prints a message according to its importance and the requested verbosity.
- Proc - Constructor in ProofAst
-
anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.
- ProcCall - Constructor in ProofAst
-
procedure call: p:tau(etl [subst], itl).
- program - Type in ProofAst
-
programs
- ProofAst - structure ProofAst
-
The First-Order LoopW Proof Checker proof abstract syntax.
- ProofAstUtils - structure ProofAstUtils
-
Utility function for the proof syntax.
- ProofChecker - structure ProofChecker
-
The First-Order LoopW Proof Checker proof checking.
- ProofEnvironment - structure ProofEnvironment
-
The First-Order LoopW Proof Checker proof environment abstract type.
- ProofPrettyPrinter - structure ProofPrettyPrinter
-
The First-Order LoopW Proof Checker proof syntax pretty-printer.
- PROOF_AST_UTILS - signature PROOF_AST_UTILS
-
Utility function for the proof syntax.
- PROOF_CHECKER - signature PROOF_CHECKER
-
The First-Order LoopW Proof Checker proof checking.
- PROOF_ENVIRONMENT - signature PROOF_ENVIRONMENT
-
The First-Order LoopW Proof Checker proof environment abstract type.
- PROOF_PRETTY_PRINTER - signature PROOF_PRETTY_PRINTER
-
The First-Order LoopW Proof Checker proof syntax pretty-printer.
- protect - Value in PrettyPrinterKeywords
-
used to encapsulate tex-math string into "".
R
- Rec - Constructor in FunAst
-
Primitive recursion: rec(t1, t2, t3).
- region - Type in Error
-
store information about the file and the position in the file.
- removeAllKey - Value in LIST_ASSOC
-
returns the association list without any association matching the given key list.
- removeAllKey - Value in ListAssoc
-
returns the association list without any association matching the given key list.
- removeKey - Value in LIST_ASSOC
-
returns the association list without any association matching the given key.
- removeKey - Value in ListAssoc
-
returns the association list without any association matching the given key.
- result - Type in SyntaxLexFun.Internal
-
- run - Value in Main
-
builds the tuple of options and calls the compiler with it.
S
- s - Value in PROOF_AST_UTILS
-
builds the successor of a term.
- s - Value in ProofAstUtils
-
builds the successor of a term.
- S - Constructor in FunAst
-
successor constructor.
- s - Value in FunTypeChecker
-
- SeqRegion - Constructor in ProofAst
-
- sequence - Type in ProofAst
-
typed sequences s |> {i}x:tau.
- someOf - Value in Main
-
gets the value in an Option, calling usage() if it is NONE.
- split - Value in PROOF_ENVIRONMENT
-
check that an identifier list is included in an environment,
returns the partition of it according to that list.
- split - Value in ProofEnvironment
-
check that an identifier list is included in an environment,
returns the partition of it according to that list.
- SSubst - Constructor in ProofAst
-
sequence substitution: s :> {i/({j}Omega)[i]} [e : (n = m)].
- Star - Constructor in ProofAst
-
null value: *.
- startpos - Value in SyntaxLexFun.UserDeclarations
-
- STARTSTATE - Constructor in SyntaxLexFun.Internal.StartStates
-
- StartStates - structure SyntaxLexFun.Internal.StartStates
-
- statedata - Type in SyntaxLexFun.Internal
-
- STRING - Value in SyntaxLexFun.Internal.StartStates
-
- stringOfCommand_internal - Value in ProofPrettyPrinter
-
converts command into string accordingly to the formula/tex demand.
- stringOfEnv - Value in FUN_PRETTY_PRINTER
-
builds a string representation of a typing environment.
- stringOfEnv - Value in FunPrettyPrinter
-
builds a string representation of a typing environment.
- stringOfExistentialIntro - Value in ProofPrettyPrinter
-
converts a substitution with an environment to a existential quantification introduction string list for ott.
- stringOfExpression - Value in PROOF_PRETTY_PRINTER
-
converts expression into string.
- stringOfExpression - Value in ProofPrettyPrinter
-
converts expression into string.
- stringOfExpressionList - Value in ProofPrettyPrinter
-
converts a list of expression into string accordingly to the formula/tex demand.
- stringOfExpression_internal - Value in ProofPrettyPrinter
-
converts expression into string accordingly to the formula/tex demand.
- stringOfIdent - Value in BASE_PRETTY_PRINTER
-
converts identifiers into string.
- stringOfIdent - Value in BasePrettyPrinter
-
converts identifiers into string.
- stringOfIdentList - Value in BASE_PRETTY_PRINTER
-
converts identifier lists into string.
- stringOfIdentList - Value in BasePrettyPrinter
-
converts identifier lists into string.
- stringOfNegExistElim - Value in ProofPrettyPrinter
-
converts a substitution with a type list to a negation existential quantification elimination string for ott.
- stringOfNegType - Value in BasePrettyPrinter
-
converts negation type into string accordingly to the formula/tex demand.
- stringOfParamList - Value in BASE_PRETTY_PRINTER
-
converts parameter list into string accordingly to the formula/tex demand.
- stringOfParamList - Value in BasePrettyPrinter
-
converts parameter list into string accordingly to the formula/tex demand.
- stringOfProcType - Value in BasePrettyPrinter
-
converts procedural type into string accordingly to the formula/tex demand.
- stringOfProgram - Value in PROOF_PRETTY_PRINTER
-
converts program into string accordingly to the formula/tex demand.
- stringOfProgram - Value in ProofPrettyPrinter
-
converts program into string accordingly to the formula/tex demand.
- stringOfProgram_Ott - Value in PROOF_PRETTY_PRINTER
-
converts program into string, generating ott-oriented type and syntax.
- stringOfProgram_Ott - Value in ProofPrettyPrinter
-
converts program into string, generating ott-oriented type and syntax.
- stringOfProgram_Untyped - Value in PROOF_PRETTY_PRINTER
-
converts program into string accordingly to the formula/tex demand,
without any type information.
- stringOfProgram_Untyped - Value in ProofPrettyPrinter
-
converts program into string accordingly to the formula/tex demand,
without any type information.
- stringOfQuantifiedTypedIdentList - Value in BASE_PRETTY_PRINTER
-
converts quantified typed identifier lists into string.
- stringOfQuantifiedTypedIdentList - Value in BasePrettyPrinter
-
converts quantified typed identifier lists into string.
- stringOfQuantifiedTypeList - Value in BASE_PRETTY_PRINTER
-
converts quantified type list into string.
- stringOfQuantifiedTypeList - Value in BasePrettyPrinter
-
converts quantified type list into string.
- stringOfSequence_internal - Value in ProofPrettyPrinter
-
converts sequence into string accordingly to the formula/tex demand.
- stringOfSubst - Value in ProofPrettyPrinter
-
converts a substitution into a string.
- stringOfTab - Value in BASE_PRETTY_PRINTER
-
builds a string with spaces for tabular display.
- stringOfTab - Value in BasePrettyPrinter
-
builds a string with spaces for tabular display.
- stringOfTerm - Value in BASE_PRETTY_PRINTER
-
converts terms abstract syntax into string.
- stringOfTerm - Value in BasePrettyPrinter
-
converts terms abstract syntax into string.
- stringOfTerm - Value in FUN_PRETTY_PRINTER
-
builds a string representation of a term.
- stringOfTerm - Value in FunPrettyPrinter
-
builds a string representation of a term.
- stringOfTerm_compact - Value in FunPrettyPrinter
-
builds a compact string representation of a term.
- stringOfTerm_expanded - Value in FunPrettyPrinter
-
builds a expanded string representation of a term.
- stringOfType - Value in BASE_PRETTY_PRINTER
-
converts formulas/types abstract syntax into string accordingly to the formula/tex demand.
- stringOfType - Value in BasePrettyPrinter
-
converts formulas/types abstract syntax into string accordingly to the formula/tex demand.
- stringOfType - Value in FUN_PRETTY_PRINTER
-
builds a string representation of a type.
- stringOfType - Value in FunPrettyPrinter
-
converts formulas/types abstract syntax into string.
- stringOfTypedExpressionList - Value in ProofPrettyPrinter
-
converts a list of typed expression into string accordingly to the formula/tex demand.
- stringOfTypedExpression_internal - Value in ProofPrettyPrinter
-
converts a pair expression * type into string accordingly to the formula/tex demand.
- stringOfTypedIdent - Value in BASE_PRETTY_PRINTER
-
converts typed identifiers into string.
- stringOfTypedIdent - Value in BasePrettyPrinter
-
converts typed identifiers into string.
- stringOfTypedIdent - Value in FunPrettyPrinter
-
converts typed identifiers into string.
- stringOfTypedIdentList - Value in BASE_PRETTY_PRINTER
-
converts typed identifier lists into string.
- stringOfTypedIdentList - Value in BasePrettyPrinter
-
converts typed identifier lists into string.
- stringOfTypedIdentList - Value in FunPrettyPrinter
-
converts typed identifier lists into string.
- stringOfValue_internal - Value in ProofPrettyPrinter
-
converts value into string accordingly to the formula/tex demand.
- subset - Value in FunTypeChecker
-
- Subst - Constructor in FunAst
-
Substitution: t {x/f[x]}[u : a = b]
- subst - Value in FunTypeChecker
-
- substitute - Value in TERMS
-
performs the substitution of a term into a formula.
- substitute - Value in Terms
-
performs the capture-avoiding substitution of a term into a formula.
- substituteAll - Value in TERMS
-
performs a substitution into a named formula list.
- substituteAll - Value in Terms
-
performs a substitution into a named formula list.
- substituteAllList - Value in TERMS
-
performs a list of substitutions into a named formula list.
- substituteAllList - Value in Terms
-
performs a list of substitutions into a named formula list.
- substituteList - Value in TERMS
-
performs a list of substitutions into a formula.
- substituteList - Value in Terms
-
performs a list of substitutions into a formula.
- subst_list - Value in FunTypeChecker
-
- subst_term - Value in FunTypeChecker
-
- Succ - Constructor in FunAst
-
Succ function.
- svalue - Type in SyntaxLexFun.UserDeclarations
-
- symb - Value in Parser
-
- SyntaxLexer - structure Parser.SyntaxLexer
-
- SyntaxLexFun - functor SyntaxLexFun
-
- SyntaxLrVals - structure Parser.SyntaxLrVals
-
- SyntaxParser - structure Parser.SyntaxParser
-
T
- T - structure SyntaxLexFun.UserDeclarations.T
-
- T - structure Parser.T
-
- tab - Value in SyntaxLexFun.Internal
-
- TBot - Constructor in ProofAst
-
absurd: _|_.
- TBot - Constructor in FunAst
-
absurd: _|_.
- TEqual - Constructor in ProofAst
-
equality predicate over terms: t = t'.
- TEqual - Constructor in FunAst
-
equality predicate over terms: t = t'.
- term - Datatype in ProofAst
-
terms in the logic.
- TERMS - signature TERMS
-
The First-Order LoopW Proof Checker formula/term substitution and alpha-equivalence.
- Terms - structure Terms
-
The First-Order LoopW Proof Checker formula/term substitution and alpha-equivalence.
- termToKeyword - Value in Parser
-
- termToString - Value in Parser
-
- term_substitute - Value in Terms
-
performs the substitution of a term into a term.
- TFun - Constructor in FunAst
-
functions: [i1, ..., in](f1 -> f2) corresponds to "forall i1...in.(f1 => f2)".
- Throw - Constructor in FunAst
-
Throw: throw t [a1, ..., an] u (with universal elimination).
- TNat - Constructor in ProofAst
-
nat predicate: nat(t) corresponds to "t in nat".
- TNat - Constructor in FunAst
-
nat predicate: nat(t) corresponds to "t in nat".
- token - Type in SyntaxLexFun.UserDeclarations
-
- Token - structure Parser.Token
-
- top - Value in PROOF_AST_UTILS
-
True type
- top - Value in ProofAstUtils
-
True type
- toString - Value in Error
-
converts line and column into a string respresentation.
- TProc - Constructor in ProofAst
-
procedures: proc(il, fl, jl, hl) corresponds to "forall il.(fl => exists jl.hl)".
- translateExpression - Value in FunTranslation
-
translate an imperative expression into a functional typed term.
- translateProgram - Value in FUN_TRANSLATION
-
translate a complete imperative program into a functional typed term.
- translateProgram - Value in FunTranslation
-
translate a complete imperative program into a functional typed term.
- translateSequence - Value in FunTranslation
-
translate an imperative sequence into a functional typed term.
- translateType - Value in FunTranslation
-
translates imperative types into functional types.
- translateValue - Value in FunTranslation
-
translate an imperative value into a functional typed term.
- tterm - Datatype in FunAst
-
functional terms.
- TTuple - Constructor in FunAst
-
tuples: [i1, ..., in](f1, ..., fm) corresponds to "exists i1...in.(f1 & ...
- Tuple - Constructor in FunAst
-
term tuples: [a1, ..., an](t1, ..., tm) (as existential introduction).
- TVar - Constructor in ProofAst
-
formula meta-variable (only used in input programs).
- TVar - Constructor in FunAst
-
type variables
- typeCheck - Value in FunTypeChecker
-
- typeCheck' - Value in FunTypeChecker
-
- typeCheckVar - Value in FunTypeChecker
-
- typed_term - Type in FunAst
-
- TypeError - Exception in FunTypeChecker
-
- typeFailureExp - Value in ProofChecker
-
- typeFailureInSeq - Value in ProofChecker
-
- typeFailureSeq - Value in ProofChecker
-
displays an error message with the current proof checking environment and the source code region.
U
- union - Value in LIST_ASSOC
-
unite to association lists.
- union - Value in ListAssoc
-
unite to association lists.
- union - Value in FunTypeChecker
-
- unionFlat - Value in LIST_ASSOC
-
unite many association lists, flattening them.
- unionFlat - Value in ListAssoc
-
unite many association lists, flattening them.
- usage - Value in Main
-
displays the compiler command usage and exits.
- UserDeclarations - structure SyntaxLexFun.UserDeclarations
-
- UTILS - signature UTILS
-
Utility functions that deals with lists.
- Utils - structure Utils
-
Utility functions that deals with lists.
V
- Val - Constructor in ProofAst
-
value.
- ValRegion - Constructor in ProofAst
-
- value - Type in ProofAst
-
typed values v : tau.
- Var - Constructor in ProofAst
-
variable declaration: var x : tau := e; s.
- vars - Value in FunTypeChecker
-
W
- writeFile - Value in Compiler
-
prints a string list to a file.
Y
- yyfinstate - Datatype in SyntaxLexFun.Internal
-
- yystartstate - Datatype in SyntaxLexFun.Internal.StartStates
-
Z
- Z - Constructor in FunAst
-
zero.
Other
- ## - Value in FunTypeChecker
-
- +! - Value in PROOF_ENVIRONMENT
-
adds an identifier typing in an environment.
- +! - Value in ProofEnvironment
-
adds an identifier typing in an environment.
- ++ - Value in PROOF_ENVIRONMENT
-
adds every typed identifiers of an environment at the end of
another environment.
- ++ - Value in ProofEnvironment
-
adds every typed identifiers of an environment at the end of
another environment.
- -! - Value in PROOF_ENVIRONMENT
-
removes an identifier typing in an environment.
- -! - Value in ProofEnvironment
-
removes an identifier typing in an environment.
- -- - Value in FunTypeChecker
-
- ? - Value in Parser
-
- @@ - Value in FunTypeChecker
-
A B C D E F G I J K L M N O P R S T U V W Y Z Other