A | |
| add [Lang.Env] | |
| add_ps [Lang.Env] | |
C | |
| check_type [Lang] |
Check that an expression has given type.
|
D | |
| dim [Lang.PS] |
Dimension of a pasting scheme.
|
E | |
| empty [Lang.Envs] |
Empty running environment.
|
| empty [Lang.Env] |
Empty environment.
|
| exec [Prover] |
Execute a command.
|
| exec [Lang] |
Execute a program.
|
| exec_cmd [Lang] |
Execute a command.
|
| exists [Lang.PS] | |
F | |
| fold_left [Lang.PS] | |
| fold_left2 [Lang.PS] | |
| fold_right [Lang.PS] | |
| free_evar [Lang] |
Free meta-variables.
|
| free_vars [Lang.PS] |
Free variables.
|
| free_vars [Lang] |
Free variables.
|
| fresh_evar [Lang] |
Generate a fresh meta-variable.
|
| fresh_inevar [Lang] | |
| fresh_var [Lang] |
Generate a fresh variable name.
|
G | |
| groupoid [Lang] |
Do we want the theory of groupoids?
|
H | |
| height [Lang.PS] |
Height of a pasting scheme.
|
I | |
| infer_type [Lang] |
Type inference.
|
| init [Prover] |
Initialize the prover.
|
| instantiate [Lang] |
Replace EVars by fresh ones.
|
| interactive [Catt] | |
L | |
| leq [Lang] |
Subtype relation between expressions.
|
| loop [Prover] |
Interactive loop.
|
M | |
| make [Lang.PS] |
Create from a context.
|
| map [Lang.PS] | |
| marker [Lang.PS] |
Dangling variable.
|
| mk [Lang] |
Create an expression from its contents.
|
N | |
| normalize [Lang] |
Normalize a value.
|
O | |
| occurs_evar [Lang] |
Whether a meta-variable occurs in a term.
|
P | |
| parametric_schemes [Lang] |
Do we allow parametric pasting schemes?
|
| parse [Prover] |
Parse a string.
|
| parse_file [Catt] | |
S | |
| show_instances [Lang] |
Do we show instance numbers in strings?
|
| source [Lang.PS] |
Source of a pasting scheme.
|
| string_of_cmd [Lang] |
String representation of a command.
|
| string_of_evar [Lang] |
String representation of a meta-variable.
|
| string_of_evarref [Lang] | |
| string_of_expr [Lang] | |
| string_of_ps [Lang] |
String representation of a pasting scheme.
|
| string_of_var [Lang] |
String representation of a variable.
|
| subst [Lang] |
Apply a parallel substitution.
|
T | |
| target [Lang.PS] |
Target of a pasting scheme.
|
| to_string [Lang.Env] |
String representation.
|
| to_string [Lang.PS] |
String representation.
|
| to_string [Lang] |
String representation of an expression.
|
| typ [Lang.Env] |
Type of an expression in an environment.
|
U | |
| unevar [Lang] |
Ensure that linked evars do not occur at toplevel.
|
| unsafe_evars [Lang] |
Do we allow unsafe uses of meta-variables?
|
| usage [Catt] | |
V | |
| value [Lang.Env] |
Value of an expression in an environment.
|