A B C D E F G I J K L M N O P R S T U V W Y Other
A
- AbsentIdent - Exception in TERM_MATCH_UNIF
-
no identifier found error
- AbsentIdent - Exception in TermMatchUnif
-
no identifier found error
- 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.
- Affect - Constructor in CoreAst
-
assignment: x := 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.
- append_with_lemma - Value in ProofDerivPrettyPrinter
-
appends a lemma number reference to a string list representing a program.
- 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 Type Inference base pretty-printer.
- BASE_PRETTY_PRINTER - signature BASE_PRETTY_PRINTER
-
The First-Order LoopW Type Inference base pretty-printer.
- Block - Constructor in ProofAst
-
block: { s }{i}x:tau
- block - Type in ProofAst
-
blocks { s |> {i'}x':tau' }{i}x:tau.
- Block - Constructor in CoreAst
-
block: { s }{i}x:tau
- block - Type in CoreAst
-
blocks.
- blockComment - Value in Parser
-
C
- Cast - Constructor in CoreAst
-
cast to a given type: e :> tau.
- Comm - Constructor in ProofAst
-
composed command: c; s.
- Comm - Constructor in CoreAst
-
composed command: c; s.
- command - Datatype in ProofAst
-
commands.
- command - Datatype in CoreAst
-
commands.
- COMMENT1 - Value in SyntaxLexFun.Internal.StartStates
-
- COMMENT2 - Value in SyntaxLexFun.Internal.StartStates
-
- CommRegion - Constructor in CoreAst
-
region used for error display.
- compile - Value in COMPILER
-
performs type inference and on-demand functional translation.
- compile - Value in Compiler
-
performs type inference and on-demand functional translation.
- COMPILER - signature COMPILER
-
The First-Order LoopW Type Inference compiler.
- Compiler - structure Compiler
-
The First-Order LoopW Type Inference compiler.
- compilerParams - Type in COMPILER
-
The type of compiling parameters.
- compilerParams - Type in Compiler
-
The type of compiling parameters.
- complete - Value in ProofDerivPrettyPrinter
-
completes to string list in order to have the same list size.
- compVersion - Value in Main
-
Current compiler version number.
- convert - Value in SyntaxLexFun.UserDeclarations
-
- CoreAst - structure CoreAst
-
The First-Order LoopW Type Inference core abstract syntax.
- CoreAstUtils - structure CoreAstUtils
-
Utility function for the core syntax.
- CorePrettyPrinter - structure CorePrettyPrinter
-
The First-Order LoopW Type Inference core syntax pretty-printer.
- CORE_AST_UTILS - signature CORE_AST_UTILS
-
Utility function for the core syntax.
- CORE_PRETTY_PRINTER - signature CORE_PRETTY_PRINTER
-
The First-Order LoopW Type Inference core syntax pretty-printer.
- Cst - Constructor in ProofAst
-
constant declaration: cst x : tau = e; s.
- Cst - Constructor in CoreAst
-
constant declaration: cst x = e; s.
- current - Value in SyntaxLexFun.UserDeclarations
-
- curstring - Value in SyntaxLexFun.UserDeclarations
-
D
- Dec - Constructor in ProofAst
-
decrementation: dec(x : tau).
- Dec - Constructor in CoreAst
-
decrementation: dec(x).
- 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 - Constructor in CoreAst
-
empty sequence.
- 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 Type Inference syntax error module.
- error - Value in Parser
-
- ERROR - Constructor in ProofInfer
-
- 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 CoreAst
-
region used for error display.
- expression - Type in ProofAst
-
typed expressions.
- expression - Datatype in CoreAst
-
expressions.
- expType - Type in CoreAst
-
formulas as in proof abstract syntax.
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].
- For - Constructor in CoreAst
-
for-loop: for I := e { s }{j}x:tau.
- formula - Datatype in ProofAst
-
first-order formulas.
- fresh - Value in TermMatchUnif
-
generates a new fresh variable.
- 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
- getEqualities - Value in ProofInfer
-
collects the equalities in two environment, discarding identities.
- getKeyList - Value in LIST_ASSOC
-
returns the list of keys.
- getKeyList - Value in ListAssoc
-
returns the list of keys.
- getMsg - Value in ProofInfer
-
builds a string with an error message, depending on the exception.
- 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 CoreAst
-
identifier.
- ident - Type in ProofAst
-
identifiers as string (numeroted for alpha-conversion).
- ident - Type in CoreAst
-
identifiers as in proof abstract syntax.
- 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).
- Inc - Constructor in CoreAst
-
incrementation: inc(x).
- inferExp - Value in ProofInfer
-
infer proof for expressions according to the loopW dependent type system.
- inferProg - Value in ProofInfer
-
infer proof for programs according to the loopW dependent type system.
- inferSeq - Value in ProofInfer
-
infer proof for sequences according to the loopW dependent type system.
- inferVal - Value in ProofInfer
-
infer proof for values according to the loopW dependent type system.
- init - Value in ProofDerivPrettyPrinter
-
Lemma counter
- INITIAL - Value in SyntaxLexFun.Internal.StartStates
-
- initLexer - Value in SyntaxLexFun.UserDeclarations
-
- instring - Value in SyntaxLexFun.UserDeclarations
-
- Int - Constructor in ProofAst
-
natural number: n.
- Int - Constructor in CoreAst
-
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, etl [subst])x:tau.
- Jump - Constructor in CoreAst
-
jump to a label: jump(k,el)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.
- Label - Constructor in CoreAst
-
label definition: k:{ s }{j}x:tau.
- leaveC - Value in SyntaxLexFun.UserDeclarations
-
- Lemma - Constructor in ProofAst
-
lemma (equation over term in a context): G |- n = m.
- lemma_fusion - Value in ProofDerivPrettyPrinter
-
concatenates two string; if they represent a lemma number reference, it
glues them together.
- LengthMismatch - Exception in TERM_MATCH_UNIF
-
length mismatch beetwen lists error
- LengthMismatch - Exception in TermMatchUnif
-
length mismatch beetwen lists error
- 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 Type Inference main program.
- makeLexer - Value in SyntaxLexFun
-
- make_spc - Value in ProofDerivPrettyPrinter
-
builds a string containing the given number of white spaces.
- match - Value in TERM_MATCH_UNIF
-
performs the pattern-matching where the pattern meta-variables
belongs to an identifiers list.
- match - Value in TermMatchUnif
-
performs the pattern-matching of formulas where the pattern meta-variables
belongs to an identifiers list.
- MatchErrorTerms - Exception in TERM_MATCH_UNIF
-
matching error for terms
- MatchErrorTerms - Exception in TermMatchUnif
-
matching error for terms
- MatchErrorTypeList - Exception in TERM_MATCH_UNIF
-
matching error for types lists
- MatchErrorTypeList - Exception in TermMatchUnif
-
matching error for types lists
- MatchErrorTypes - Exception in TERM_MATCH_UNIF
-
matching error for types
- MatchErrorTypes - Exception in TermMatchUnif
-
matching error for types
- matchList - Value in TERM_MATCH_UNIF
-
performs the pattern-matching of a formulas list with a patterns list
where the pattern meta-variables belongs to an identifiers list.
- matchList - Value in TermMatchUnif
-
performs the pattern-matching of a formulas list with a patterns list
where the pattern meta-variables belongs to an identifiers list.
- matchOrderedList - Value in TERM_MATCH_UNIF
-
performs the pattern-matching of a formulas list with a patterns list
where the pattern meta-variables belongs to an identifiers list.
- matchOrderedList - Value in TermMatchUnif
-
performs the pattern-matching of a formulas list with a patterns list
where the pattern meta-variables belongs to an identifiers list.
- matchUnif - Value in TermMatchUnif
-
performs the pattern-matching and unification where the pattern meta-variables
belongs to an identifiers list.
- MatchUnifErrorTerms - Exception in TERM_MATCH_UNIF
-
matching+unification error for terms
- MatchUnifErrorTerms - Exception in TermMatchUnif
-
matching+unification error for terms
- MatchUnifErrorTypeList - Exception in TERM_MATCH_UNIF
-
matching+unification error for types lists
- MatchUnifErrorTypeList - Exception in TermMatchUnif
-
matching+unification error for types lists
- MatchUnifErrorTypes - Exception in TERM_MATCH_UNIF
-
matching+unification error for types
- MatchUnifErrorTypes - Exception in TermMatchUnif
-
matching+unification error for types
- matchUnifList - Value in TERM_MATCH_UNIF
-
performs the pattern-matching and unification where the pattern meta-variables
belongs to an identifiers list.
- matchUnifList - Value in TermMatchUnif
-
performs the pattern-matching and unification where the pattern meta-variables
belongs to an identifiers list.
- math - Value in PrettyPrinterKeywords
-
used to encapsulate tex-math string into $.
- max_width - Value in ProofDerivPrettyPrinter
-
calculates the longest string in a string list.
- 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 CORE_AST_UTILS
-
builds an unary natural number from an int.
- mkNat - Value in CoreAstUtils
-
builds an unary natural number from an int.
- mk_exp_subst_lemma - Value in ProofInfer
-
builds a substitution derivation for an expression.
- mk_seq_subst_lemma - Value in ProofInfer
-
builds a substitution derivation for a sequence.
N
- N - Constructor in SyntaxLexFun.Internal
-
- newline - Value in SyntaxLexFun.UserDeclarations
-
- newS - Value in SyntaxLexFun.UserDeclarations
-
- new_term_subst - Value in TermMatchUnif
-
builds a new unification equation with a fresh identifier.
- new_term_subst_eq - Value in TermMatchUnif
-
builds a new unification equation with a fresh identifier.
- next - Value in ProofDerivPrettyPrinter
-
Lemma counter
- NotUnifyableTerms - Exception in TERM_MATCH_UNIF
-
unification error for terms
- NotUnifyableTerms - Exception in TermMatchUnif
-
unification error for terms
- NotUnifyableTypes - Exception in TERM_MATCH_UNIF
-
unification error for types
- NotUnifyableTypes - Exception in TermMatchUnif
-
unification error for types
O
- OK - Constructor in ProofInfer
-
- optFail - Value in Error
-
calls either fail or failm depending on the region Option.
P
- p - Value in CORE_AST_UTILS
-
builds the predecessor of a term.
- p - Value in CoreAstUtils
-
builds the predecessor of a term.
- 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
-
- PrettyPrinterKeywords - structure PrettyPrinterKeywords
-
The First-Order LoopW Type Inference pretty-printer keywords for abstract syntax.
- PRETTY_PRINTER_KEYWORDS - signature PRETTY_PRINTER_KEYWORDS
-
The First-Order LoopW Type Inference 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.
- Proc - Constructor in CoreAst
-
anonymous procedure declaration: proc({il} in xfl; {jl} out yfl){ s }{jl}yfl.
- ProcCall - Constructor in ProofAst
-
procedure call: p:tau(etl [subst], itl).
- ProcCall - Constructor in CoreAst
-
procedure call: p(el, il).
- program - Type in ProofAst
-
programs
- program - Type in CoreAst
-
programs.
- ProofAst - structure ProofAst
-
The First-Order LoopW Type Inference proof abstract syntax.
- ProofDerivPrettyPrinter - structure ProofDerivPrettyPrinter
-
The First-Order LoopW Type Inference proof derivation pretty-printer.
- ProofEnvironment - structure ProofEnvironment
-
The First-Order LoopW Type Inference proof environment abstract type.
- proofInfer - Value in PROOF_INFER
-
returns the complete proof.
- proofInfer - Value in ProofInfer
-
returns the complete proof.
- ProofInfer - structure ProofInfer
-
The First-Order LoopW Type Inference proof inference.
- ProofPrettyPrinter - structure ProofPrettyPrinter
-
The First-Order LoopW Type Inference proof syntax pretty-printer.
- PROOF_DERIV_PRETTY_PRINTER - signature PROOF_DERIV_PRETTY_PRINTER
-
The First-Order LoopW Type Inference proof derivation pretty-printer.
- PROOF_ENVIRONMENT - signature PROOF_ENVIRONMENT
-
The First-Order LoopW Type Inference proof environment abstract type.
- PROOF_INFER - signature PROOF_INFER
-
The First-Order LoopW Type Inference proof inference.
- PROOF_PRETTY_PRINTER - signature PROOF_PRETTY_PRINTER
-
The First-Order LoopW Type Inference proof syntax pretty-printer.
- protect - Value in PrettyPrinterKeywords
-
used to encapsulate tex-math string into "".
R
- 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.
- removeRegionCommand - Value in CoreAstUtils
-
removes regions in commands abstract syntax.
- removeRegionExpression - Value in CORE_AST_UTILS
-
removes regions in expressions abstract syntax.
- removeRegionExpression - Value in CoreAstUtils
-
removes regions in expressions abstract syntax.
- removeRegionProgram - Value in CORE_AST_UTILS
-
removes regions in programs abstract syntax.
- removeRegionProgram - Value in CoreAstUtils
-
removes regions in programs abstract syntax.
- removeRegionSequence - Value in CoreAstUtils
-
removes regions in sequences abstract syntax.
- removeRegionValue - Value in CoreAstUtils
-
removes regions in values abstract syntax.
- result - Type in SyntaxLexFun.Internal
-
- result - Datatype in ProofInfer
-
result type, either OK or ERROR with information enough to display an error message.
- run - Value in Main
-
builds the tuple of options and calls the compiler with it.
S
- s - Value in CORE_AST_UTILS
-
builds the successor of a term.
- s - Value in CoreAstUtils
-
builds the successor of a term.
- SeqRegion - Constructor in CoreAst
-
region used for error display.
- sequence - Type in ProofAst
-
typed sequences.
- sequence - Datatype in CoreAst
-
sequences.
- 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: *.
- Star - Constructor in CoreAst
-
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
-
- stringOfBlock_internal - Value in CorePrettyPrinter
-
converts block into string accordingly to the formula/tex demand.
- stringOfCommand - Value in CORE_PRETTY_PRINTER
-
converts command into string accordingly to the formula/tex demand.
- stringOfCommand - Value in CorePrettyPrinter
-
converts command into string accordingly to the formula/tex demand.
- stringOfCommand - Value in ProofDerivPrettyPrinter
-
converts command typing derivation into string accordingly to the formula/tex demand.
- stringOfCommand_internal - Value in CorePrettyPrinter
-
converts command into string accordingly to the formula/tex demand.
- stringOfCommand_internal - Value in ProofPrettyPrinter
-
converts command into string accordingly to the formula/tex demand.
- stringOfExistentialIntro - Value in ProofPrettyPrinter
-
converts a substitution with an environment to a existential quantification introduction string list for ott.
- stringOfExpression - Value in CORE_PRETTY_PRINTER
-
converts expression into string accordingly to the formula/tex demand.
- stringOfExpression - Value in CorePrettyPrinter
-
converts expression into string accordingly to the formula/tex demand.
- stringOfExpression - Value in ProofDerivPrettyPrinter
-
converts expression typing derivation into string accordingly to the formula/tex demand.
- stringOfExpressionList - Value in CorePrettyPrinter
-
converts expression list into string accordingly to the formula/tex demand.
- stringOfExpressionList - Value in ProofPrettyPrinter
-
converts a list of expression into string accordingly to the formula/tex demand.
- stringOfExpressionList - Value in ProofDerivPrettyPrinter
-
converts expression list into string accordingly to the formula/tex demand.
- stringOfExpression_internal - Value in CorePrettyPrinter
-
converts 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 CORE_PRETTY_PRINTER
-
converts program into string accordingly to the formula/tex demand.
- stringOfProgram - Value in CorePrettyPrinter
-
converts program 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 CORE_PRETTY_PRINTER
-
converts program into string accordingly to the formula/tex demand,
without any type information.
- stringOfProgram_Untyped - Value in CorePrettyPrinter
-
converts program into string accordingly to the formula/tex demand,
without any type information.
- 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 - Value in CORE_PRETTY_PRINTER
-
converts sequence into string accordingly to the formula/tex demand.
- stringOfSequence - Value in CorePrettyPrinter
-
converts sequence into string accordingly to the formula/tex demand.
- stringOfSequence - Value in ProofDerivPrettyPrinter
-
converts sequence typing derivation into string accordingly to the formula/tex demand.
- stringOfSequence_internal - Value in CorePrettyPrinter
-
converts sequence into string accordingly to the formula/tex demand.
- 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.
- stringOfTab_T - Value in ProofDerivPrettyPrinter
-
builds a string with | and spaces for typing tabular display.
- stringOfTerm - Value in BASE_PRETTY_PRINTER
-
converts terms abstract syntax into string.
- stringOfTerm - Value in BasePrettyPrinter
-
converts terms abstract syntax into string.
- 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.
- 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.
- stringOfTypedIdentList - Value in BASE_PRETTY_PRINTER
-
converts typed identifier lists into string.
- stringOfTypedIdentList - Value in BasePrettyPrinter
-
converts typed identifier lists into string.
- stringOfTyping - Value in PROOF_DERIV_PRETTY_PRINTER
-
converts program with typing derivation into string
accordingly to the formula/tex demand.
- stringOfTyping - Value in ProofDerivPrettyPrinter
-
converts program with typing derivation into string
accordingly to the formula/tex demand.
- stringOfValue - Value in CORE_PRETTY_PRINTER
-
converts value into string accordingly to the formula/tex demand.
- stringOfValue - Value in CorePrettyPrinter
-
converts value into string accordingly to the formula/tex demand.
- stringOfValue - Value in ProofDerivPrettyPrinter
-
converts value typing derivation into string accordingly to the formula/tex demand.
- stringOfValue_internal - Value in CorePrettyPrinter
-
converts value into string accordingly to the formula/tex demand.
- stringOfValue_internal - Value in ProofPrettyPrinter
-
converts value into string accordingly to the formula/tex demand.
- 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.
- 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
-
- tabulate - Value in ProofDerivPrettyPrinter
-
appends at the end of each string of a string list an amount of white
spaces in order to have exactly string of the same given size.
- TBot - Constructor in ProofAst
-
absurd: _|_.
- TEqual - Constructor in ProofAst
-
equality predicate over terms: t = t'.
- term - Datatype in ProofAst
-
terms in the logic.
- term - Type in CoreAst
-
terms as in proof abstract syntax.
- TermMatchUnif - structure TermMatchUnif
-
The First-Order LoopW Type Inference formula/term matching and unification.
- TERMS - signature TERMS
-
The First-Order LoopW Type Inference formula/term substitution and alpha-equivalence.
- Terms - structure Terms
-
The First-Order LoopW Type Inference formula/term substitution and alpha-equivalence.
- termToKeyword - Value in Parser
-
- termToString - Value in Parser
-
- term_match - Value in TermMatchUnif
-
performs the pattern-matching of terms where the pattern meta-variables
belongs to an identifiers list.
- term_matchUnif - Value in TermMatchUnif
-
performs the pattern-matching and unification where the pattern meta-variables
belongs to an identifiers list.
- TERM_MATCH_UNIF - signature TERM_MATCH_UNIF
-
The First-Order LoopW Type Inference formula/term matching and unification.
- term_substitute - Value in Terms
-
performs the substitution of a term into a term.
- term_unify - Value in TermMatchUnif
-
performs the unification of two terms.
- TNat - Constructor in ProofAst
-
nat predicate: nat(t) corresponds to "t in nat".
- token - Type in SyntaxLexFun.UserDeclarations
-
- Token - structure Parser.Token
-
- top - Value in CORE_AST_UTILS
-
True type
- top - Value in CoreAstUtils
-
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)".
- TVar - Constructor in ProofAst
-
formula meta-variable (only used in input programs).
- typedIdent - Type in CoreAst
-
typed identifiers.
U
- unify - Value in TERM_MATCH_UNIF
-
performs the unification of two formulas on the term-level.
- unify - Value in TermMatchUnif
-
performs the unification of two formulas on the term-level.
- unifyList - Value in TERM_MATCH_UNIF
-
performs the unification of two (identifiers, formulas) list on the term-level.
- unifyList - Value in TermMatchUnif
-
performs the unification of two (identifiers, formulas) list on the term-level.
- unifyOrderedList - Value in TERM_MATCH_UNIF
-
performs the unification of two formulas list on the term-level.
- unifyOrderedList - Value in TermMatchUnif
-
performs the unification of two formulas list on the term-level.
- union - Value in LIST_ASSOC
-
unite to association lists.
- union - Value in ListAssoc
-
unite to association lists.
- 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.
- Val - Constructor in CoreAst
-
value.
- ValRegion - Constructor in CoreAst
-
region used for error display.
- value - Type in ProofAst
-
typed values.
- value - Datatype in CoreAst
-
values.
- Var - Constructor in ProofAst
-
variable declaration: var x : tau := e; s.
- Var - Constructor in CoreAst
-
variable declaration: var x := e; s.
W
- writeFile - Value in Compiler
-
prints a string list to a file.
Y
- yyfinstate - Datatype in SyntaxLexFun.Internal
-
- yystartstate - Datatype in SyntaxLexFun.Internal.StartStates
-
Other
- +! - 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 Parser
-
A B C D E F G I J K L M N O P R S T U V W Y Other