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 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

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 Z Other