Overview  Index  Help 
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

Overview  Index  Help 
A B C D E F G I J K L M N O P R S T U V W Y Other