| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1113 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (145 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (226 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (238 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (276 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Global Index
A
A [inductive, in Icharate.Examples.polEx]a [constructor, in Icharate.Examples.polEx]
A [inductive, in Icharate.Examples.medialEx]
A [inductive, in Icharate.Examples.dep_ex]
A [inductive, in Icharate.Examples.ex1]
a [constructor, in Icharate.Examples.ex1]
A [inductive, in Icharate.Examples.ex1s]
a [constructor, in Icharate.Examples.ex1s]
A [projection, in Icharate.Kernel.semLex]
abs [constructor, in Icharate.Kernel.lambda_bruijn]
absRed [constructor, in Icharate.Kernel.lambda_reduction]
absRed2 [constructor, in Icharate.Kernel.lambda_reduction]
access [definition, in Icharate.Kernel.basics]
access_eq_apply [lemma, in Icharate.Kernel.apply_rule_props]
access_subCont [lemma, in Icharate.Kernel.apply_rule_props]
access_sub_cont [lemma, in Icharate.Kernel.apply_rule_props]
access_par_replace [definition, in Icharate.Kernel.apply_rule_props]
access_same_shape [lemma, in Icharate.Kernel.apply_rule_props]
access_same_shape_true [lemma, in Icharate.Kernel.apply_rule_props]
access_pathR [lemma, in Icharate.Kernel.apply_rule_props]
access_pathL [lemma, in Icharate.Kernel.apply_rule_props]
access_leaf_false [lemma, in Icharate.Kernel.apply_rule_props]
access_is_sub_cont [lemma, in Icharate.Kernel.apply_rule_props]
access_leaf [lemma, in Icharate.Kernel.apply_rule_props]
access_dec [lemma, in Icharate.Kernel.apply_rule_props]
access_some_true [lemma, in Icharate.Kernel.apply_rule_props]
access_diam_none [lemma, in Icharate.Kernel.apply_rule_props]
access_diam_TDiam [lemma, in Icharate.Kernel.apply_rule_props]
access_diam_some [lemma, in Icharate.Kernel.apply_rule_props]
access_Com_some [lemma, in Icharate.Kernel.apply_rule_props]
access_com_some [lemma, in Icharate.Kernel.apply_rule_props]
access_com_none [lemma, in Icharate.Kernel.apply_rule_props]
access_res [lemma, in Icharate.Kernel.apply_rule_props]
access_tac [definition, in Icharate.Tacs.tacticsDed]
acces_same_shape [lemma, in Icharate.Kernel.apply_rule_props]
acces_isLeaf [lemma, in Icharate.Kernel.apply_rule_props]
acces_leaf_shape [lemma, in Icharate.Kernel.apply_rule_props]
addToEnd [definition, in Icharate.Meta.unbounDep]
add_extension [definition, in Icharate.Kernel.basics]
add_rule [constructor, in Icharate.Kernel.basics]
add_next [constructor, in Icharate.Kernel.lambda_bruijn]
add_0 [constructor, in Icharate.Kernel.lambda_bruijn]
add_ith_list [inductive, in Icharate.Kernel.lambda_bruijn]
add_in [lemma, in Icharate.Lib.permutation]
add_2 [constructor, in Icharate.Lib.permutation]
add_fst [constructor, in Icharate.Lib.permutation]
add_somewhere [inductive, in Icharate.Lib.permutation]
add_in [lemma, in Icharate.Lib.listAux]
allDistinctLeaves [definition, in Icharate.Kernel.basics]
allDistinct_to_distinct [lemma, in Icharate.Kernel.basics]
allSem [section, in Icharate.Kernel.lambda_bruijn]
allSem.A [variable, in Icharate.Kernel.lambda_bruijn]
allSem.I [variable, in Icharate.Kernel.lambda_bruijn]
allSem.J [variable, in Icharate.Kernel.lambda_bruijn]
allSem.lambdaX [section, in Icharate.Kernel.lambda_bruijn]
allSem.lambdaX.getSemTypeX [variable, in Icharate.Kernel.lambda_bruijn]
allSem.lambdaX.X [variable, in Icharate.Kernel.lambda_bruijn]
allSem.map [variable, in Icharate.Kernel.lambda_bruijn]
AND [constructor, in Icharate.Kernel.logic_const]
appl [constructor, in Icharate.Kernel.lambda_bruijn]
application_r [definition, in Icharate.Meta.derivedRulesNatDed]
application_l [definition, in Icharate.Meta.derivedRulesNatDed]
applRed1 [constructor, in Icharate.Kernel.lambda_reduction]
applRed2 [constructor, in Icharate.Kernel.lambda_reduction]
apply_rule [definition, in Icharate.Kernel.basics]
apply_rule_par_replace [definition, in Icharate.Kernel.apply_rule_props]
apply_rule_same_shape2 [lemma, in Icharate.Kernel.apply_rule_props]
apply_rule_same_shape [lemma, in Icharate.Kernel.apply_rule_props]
apply_rule_diam [lemma, in Icharate.Kernel.apply_rule_props]
apply_rule_com [lemma, in Icharate.Kernel.apply_rule_props]
apply_rule_pvar [lemma, in Icharate.Kernel.apply_rule_props]
apply_rule_tac [definition, in Icharate.Tacs.tacticsDed]
apply_rule_props [library]
argument_lowering [definition, in Icharate.Meta.derivedRulesNatDed]
At [constructor, in Icharate.Kernel.basics]
Ax [constructor, in Icharate.Kernel.sequent]
axiomGen [definition, in Icharate.Meta.derivedRulesNatDed]
A_syn [projection, in Icharate.Kernel.natDedGram]
B
BackE [constructor, in Icharate.Kernel.natDed]BackI [constructor, in Icharate.Kernel.natDed]
Backslash [constructor, in Icharate.Kernel.basics]
Back_antitonicity [lemma, in Icharate.Meta.derivedRulesNatDed]
Back_lifting [definition, in Icharate.Meta.derivedRulesNatDed]
bapply_rule [axiom, in Icharate.Kernel.basics]
basics [library]
bComma [constructor, in Icharate.Kernel.basics]
bcontext [inductive, in Icharate.Kernel.basics]
bDiamond [constructor, in Icharate.Kernel.basics]
beta [section, in Icharate.Kernel.lambda_reduction]
betaExtract [lemma, in Icharate.Kernel.lambda_reduction]
betaRefl [constructor, in Icharate.Kernel.lambda_reduction]
betaTrans [constructor, in Icharate.Kernel.lambda_reduction]
betaTransitive [lemma, in Icharate.Kernel.lambda_reduction]
beta_normal [lemma, in Icharate.Kernel.lambda_reduction]
beta_twoL_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_twoL_mono2 [lemma, in Icharate.Kernel.lambda_reduction]
beta_twoL_mono1 [lemma, in Icharate.Kernel.lambda_reduction]
beta_dediam_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_diam_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_debox_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_pi2_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_pi1_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_box_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_abs_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_app_mono [lemma, in Icharate.Kernel.lambda_reduction]
beta_app_mono2 [lemma, in Icharate.Kernel.lambda_reduction]
beta_app_mono1 [lemma, in Icharate.Kernel.lambda_reduction]
beta_reduction [inductive, in Icharate.Kernel.lambda_reduction]
beta_one_step [inductive, in Icharate.Kernel.lambda_reduction]
beta.X [variable, in Icharate.Kernel.lambda_reduction]
Box [constructor, in Icharate.Kernel.basics]
box [constructor, in Icharate.Kernel.lambda_bruijn]
boxDeboxRed [constructor, in Icharate.Kernel.lambda_reduction]
boxDiam [definition, in Icharate.Meta.derivedRulesNatDed]
BoxE [constructor, in Icharate.Kernel.natDed]
BoxI [constructor, in Icharate.Kernel.natDed]
boxRed [constructor, in Icharate.Kernel.lambda_reduction]
box_coq [axiom, in Icharate.Kernel.lambda_coq]
box2diam [definition, in Icharate.Meta.derivedRulesNatDed]
C
cartProd [constructor, in Icharate.Kernel.lambda_bruijn]classes [section, in Icharate.Kernel.struct_props]
classes.I [variable, in Icharate.Kernel.struct_props]
classes.J [variable, in Icharate.Kernel.struct_props]
clause [definition, in Icharate.Examples.ex1]
clause [definition, in Icharate.Examples.ex1s]
clause_tree [definition, in Icharate.Examples.ex1]
comDiam [definition, in Icharate.Kernel.struct_ex]
comDiamImgInv [lemma, in Icharate.Kernel.struct_ex]
comDiam_Inv [lemma, in Icharate.Kernel.struct_ex]
comDiam_rw [lemma, in Icharate.Kernel.struct_ex]
Comma [constructor, in Icharate.Kernel.basics]
comma_matches [constructor, in Icharate.Kernel.basics]
compile [definition, in Icharate.Kernel.basics]
compile_tac [definition, in Icharate.Tacs.tacticsDed]
completement [constructor, in Icharate.Examples.medialEx]
composition_Back [definition, in Icharate.Meta.derivedRulesNatDed]
composition_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
comW [constructor, in Icharate.Tacs.tacticsDed]
com_eqv [constructor, in Icharate.Kernel.basics]
condExt [definition, in Icharate.Meta.unaries]
condStruct [definition, in Icharate.Meta.unaries]
consT [constructor, in Icharate.Kernel.lambda_coq]
constructList [definition, in Icharate.Tacs.tacticsDed]
constructList [definition, in Icharate.Lib.listAux]
cons_trans [constructor, in Icharate.Kernel.lambda_coq]
cont [definition, in Icharate.Examples.polEx]
containsNoRedex [definition, in Icharate.Kernel.lambda_reduction]
context [inductive, in Icharate.Kernel.basics]
contextToForm [definition, in Icharate.Kernel.basics]
contextW [inductive, in Icharate.Tacs.tacticsDed]
context_eqv [inductive, in Icharate.Kernel.basics]
context_equiv [definition, in Icharate.Kernel.basics]
context_strip [definition, in Icharate.Kernel.basics]
context_inject [definition, in Icharate.Kernel.basics]
coq_terms.consts [variable, in Icharate.Kernel.lambda_coq]
coq_terms.getSemTypeX [variable, in Icharate.Kernel.lambda_coq]
coq_terms.X [variable, in Icharate.Kernel.lambda_coq]
coq_terms [section, in Icharate.Kernel.lambda_coq]
countDiam [definition, in Icharate.Kernel.struct_props]
co_application_r [definition, in Icharate.Meta.derivedRulesNatDed]
co_application_l [definition, in Icharate.Meta.derivedRulesNatDed]
crossDep [library]
cross_depend [definition, in Icharate.Meta.crossDep]
cross_dep.R [variable, in Icharate.Meta.crossDep]
cross_dep.eqdecW [variable, in Icharate.Meta.crossDep]
cross_dep.eqdecA [variable, in Icharate.Meta.crossDep]
cross_dep.eqdecJ [variable, in Icharate.Meta.crossDep]
cross_dep.eqdecI [variable, in Icharate.Meta.crossDep]
cross_dep.W [variable, in Icharate.Meta.crossDep]
cross_dep.A [variable, in Icharate.Meta.crossDep]
cross_dep.J [variable, in Icharate.Meta.crossDep]
cross_dep.I [variable, in Icharate.Meta.crossDep]
cross_dep [section, in Icharate.Meta.crossDep]
cst [inductive, in Icharate.Kernel.final_sem]
currying_Back [definition, in Icharate.Meta.derivedRulesNatDed]
currying_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
CutRule [constructor, in Icharate.Kernel.sequent]
cut_rule' [definition, in Icharate.Meta.derivedRulesNatDed]
cut_rule1 [definition, in Icharate.Meta.derivedRulesNatDed]
cut_rule [definition, in Icharate.Meta.derivedRulesNatDed]
D
debox [constructor, in Icharate.Kernel.lambda_bruijn]deboxRed [constructor, in Icharate.Kernel.lambda_reduction]
debox_coq [axiom, in Icharate.Kernel.lambda_coq]
dediam [constructor, in Icharate.Kernel.lambda_bruijn]
dediamRed [constructor, in Icharate.Kernel.lambda_reduction]
dediam_coq [axiom, in Icharate.Kernel.lambda_coq]
deep_to_shallow [definition, in Icharate.Kernel.interp_coq]
Definitions [section, in Icharate.Kernel.basics]
Definitions.Main [section, in Icharate.Kernel.basics]
Definitions.Main.formulae_etc.W [variable, in Icharate.Kernel.basics]
Definitions.Main.formulae_etc.A [variable, in Icharate.Kernel.basics]
Definitions.Main.formulae_etc [section, in Icharate.Kernel.basics]
Definitions.Main.I [variable, in Icharate.Kernel.basics]
Definitions.Main.J [variable, in Icharate.Kernel.basics]
Definitions.Main.rep [section, in Icharate.Kernel.basics]
Definitions.Main.rep.A [variable, in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.Ru [variable, in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.decJ [variable, in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.decI [variable, in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def [section, in Icharate.Kernel.basics]
Definitions.Main.rep.W [variable, in Icharate.Kernel.basics]
defs [section, in Icharate.Kernel.sequent]
defs.A [variable, in Icharate.Kernel.sequent]
defs.decI [variable, in Icharate.Kernel.sequent]
defs.decJ [variable, in Icharate.Kernel.sequent]
defs.I [variable, in Icharate.Kernel.sequent]
defs.J [variable, in Icharate.Kernel.sequent]
defs.R [variable, in Icharate.Kernel.sequent]
defs.W [variable, in Icharate.Kernel.sequent]
dep_ex [library]
derivedRulesNatDed [library]
deriveTo [definition, in Icharate.Kernel.semLex]
deriveToSyn [definition, in Icharate.Kernel.natDedGram]
derivSem [library]
deriv1 [lemma, in Icharate.Examples.polEx]
deriv1 [definition, in Icharate.Examples.ex1]
deriv1 [definition, in Icharate.Examples.ex1s]
deriv2 [definition, in Icharate.Examples.ex1]
De_currying_Back [definition, in Icharate.Meta.derivedRulesNatDed]
De_currying_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
diam [constructor, in Icharate.Kernel.lambda_bruijn]
diamBox [definition, in Icharate.Meta.derivedRulesNatDed]
diamDediamRed [constructor, in Icharate.Kernel.lambda_reduction]
DiamE [constructor, in Icharate.Kernel.natDed]
DiamI [constructor, in Icharate.Kernel.natDed]
Diamond [constructor, in Icharate.Kernel.basics]
DiamondE' [definition, in Icharate.Kernel.natDed]
diamRed [constructor, in Icharate.Kernel.lambda_reduction]
diamW [constructor, in Icharate.Tacs.tacticsDed]
diam_coq [axiom, in Icharate.Kernel.lambda_coq]
diam_Box [definition, in Icharate.Meta.derivedRulesNatDed]
diam_eqv [constructor, in Icharate.Kernel.basics]
diam_matches [constructor, in Icharate.Kernel.basics]
diffDBTerm [definition, in Icharate.Meta.unaries]
diffDiamBox [definition, in Icharate.Meta.unaries]
distDiam [definition, in Icharate.Meta.crossDep]
distinct_add [lemma, in Icharate.Lib.listAux]
distinct_app [lemma, in Icharate.Lib.listAux]
distinct_elts [definition, in Icharate.Lib.listAux]
Dot [constructor, in Icharate.Kernel.basics]
DotE [constructor, in Icharate.Kernel.natDed]
DotE' [definition, in Icharate.Kernel.natDed]
DotI [constructor, in Icharate.Kernel.natDed]
Dot_monotonicity0 [lemma, in Icharate.Meta.derivedRulesNatDed]
Dot_monotonicity [lemma, in Icharate.Meta.derivedRulesNatDed]
doubleReplacePar [definition, in Icharate.Kernel.basics]
dP [constructor, in Icharate.Tacs.tacticsDed]
E
E [axiom, in Icharate.Kernel.lambda_coq]e [constructor, in Icharate.Kernel.lambda_bruijn]
eqdec [definition, in Icharate.Kernel.basics]
eqdecA [definition, in Icharate.Examples.polEx]
eqdecA [definition, in Icharate.Examples.medialEx]
eqdecA [definition, in Icharate.Examples.dep_ex]
eqdecA [definition, in Icharate.Examples.ex1]
eqdecA [definition, in Icharate.Examples.ex1s]
eqdecA [projection, in Icharate.Kernel.semLex]
eqdecA_syn [projection, in Icharate.Kernel.natDedGram]
eqdecC [definition, in Icharate.Kernel.basics]
eqDecF [definition, in Icharate.Kernel.basics]
eqdecI [definition, in Icharate.Examples.polEx]
eqdecI [definition, in Icharate.Examples.medialEx]
eqdecI [definition, in Icharate.Examples.dep_ex]
eqdecI [definition, in Icharate.Examples.ex1]
eqdecI [definition, in Icharate.Examples.ex1s]
eqdecI [projection, in Icharate.Kernel.semLex]
eqdecI_syn [projection, in Icharate.Kernel.natDedGram]
eqdecJ [definition, in Icharate.Examples.polEx]
eqdecJ [definition, in Icharate.Examples.medialEx]
eqdecJ [definition, in Icharate.Examples.dep_ex]
eqdecJ [definition, in Icharate.Examples.ex1]
eqdecJ [definition, in Icharate.Examples.ex1s]
eqdecJ [projection, in Icharate.Kernel.semLex]
eqdecJ_syn [projection, in Icharate.Kernel.natDedGram]
eqdecRess [definition, in Icharate.Kernel.basics]
eqDecSem [definition, in Icharate.Kernel.lambda_bruijn]
eqdecX_rw [lemma, in Icharate.Tacs.struct_tacs]
eqDiffDB [lemma, in Icharate.Meta.unaries]
eqDiffDiamBox [lemma, in Icharate.Meta.unaries]
eqmset_to_ind [lemma, in Icharate.Lib.permutation]
EX [constructor, in Icharate.Kernel.logic_const]
exchange_r [definition, in Icharate.Meta.derivedRulesNatDed]
exchange_l [definition, in Icharate.Meta.derivedRulesNatDed]
excons [constructor, in Icharate.Lib.listAux]
exnil [constructor, in Icharate.Lib.listAux]
ext [definition, in Icharate.Examples.ex1s]
ext [projection, in Icharate.Kernel.semLex]
extension [inductive, in Icharate.Kernel.basics]
extractNF [definition, in Icharate.Kernel.lambda_reduction]
extract_lex_syn [definition, in Icharate.Kernel.semLex]
extract_sub_list [definition, in Icharate.Kernel.semLex]
extract_forall [lemma, in Icharate.Lib.listAux]
extract_permut [lemma, in Icharate.Lib.listAux]
extract_app [lemma, in Icharate.Lib.listAux]
extract_one [lemma, in Icharate.Lib.listAux]
extract_opt [inductive, in Icharate.Lib.listAux]
ext_syn [projection, in Icharate.Kernel.natDedGram]
ext1 [definition, in Icharate.Examples.polEx]
ext1 [definition, in Icharate.Examples.medialEx]
ext1 [definition, in Icharate.Examples.dep_ex]
ext1 [definition, in Icharate.Examples.ex1]
EXU [constructor, in Icharate.Kernel.logic_const]
ex1 [library]
ex1s [library]
ex3 [library]
F
fill [definition, in Icharate.Kernel.basics]fill_to_par_replace [definition, in Icharate.Kernel.basics]
final_sem [library]
fitsContSent [definition, in Icharate.Kernel.natDedGram]
fits_aux [definition, in Icharate.Kernel.natDedGram]
flattenCont [definition, in Icharate.Kernel.natDedGram]
flatten_pattern [definition, in Icharate.Kernel.basics]
FORALL [constructor, in Icharate.Kernel.logic_const]
forall_eq_list [lemma, in Icharate.Lib.listAux]
form [constructor, in Icharate.Kernel.basics]
Form [inductive, in Icharate.Kernel.basics]
formal [constructor, in Icharate.Kernel.final_sem]
form_eqv [constructor, in Icharate.Kernel.basics]
form_matches [constructor, in Icharate.Kernel.basics]
frag [definition, in Icharate.Examples.medialEx]
free_lambda [definition, in Icharate.Kernel.derivSem]
funAppli [constructor, in Icharate.Kernel.lambda_bruijn]
G
Geach_secondary_Back [definition, in Icharate.Meta.derivedRulesNatDed]Geach_secondary_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
Geach_main_Back [definition, in Icharate.Meta.derivedRulesNatDed]
Geach_main_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
Geach_main_Back [definition, in Icharate.Examples.ex3]
gentzen [inductive, in Icharate.Kernel.sequent]
getContext [definition, in Icharate.Tacs.tacticsDed]
getContext1 [definition, in Icharate.Tacs.tacticsDed]
getFirstPathDiam [definition, in Icharate.Tacs.tacticsDed]
getHypForm [definition, in Icharate.Tacs.tacticsDed]
getIthRule [definition, in Icharate.Tacs.tacticsDed]
getSemantic [definition, in Icharate.Kernel.derivSem]
getSubLists [definition, in Icharate.Lib.listAux]
getTermByPath [definition, in Icharate.Tacs.tacticsDed]
getTypeAbs [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeAppl [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeBox [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeDebox [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeDediam [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeDiam [lemma, in Icharate.Kernel.lambda_bruijn]
getTypePi1 [lemma, in Icharate.Kernel.lambda_bruijn]
getTypePi2 [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeTwoL [lemma, in Icharate.Kernel.lambda_bruijn]
getTypeWT [definition, in Icharate.Kernel.derivSem]
gram1 [definition, in Icharate.Examples.polEx]
gram1 [definition, in Icharate.Examples.medialEx]
gram1 [definition, in Icharate.Examples.dep_ex]
gram1 [definition, in Icharate.Examples.ex1]
gram2 [definition, in Icharate.Examples.ex1s]
H
hasNF1 [constructor, in Icharate.Kernel.lambda_reduction]hasNormalForm [inductive, in Icharate.Kernel.lambda_reduction]
hasSubContexts [inductive, in Icharate.Kernel.basics]
has_pdiam [constructor, in Icharate.Kernel.basics]
has_pcom [constructor, in Icharate.Kernel.basics]
has_pvar [constructor, in Icharate.Kernel.basics]
hComma [constructor, in Icharate.Kernel.basics]
hcontext [inductive, in Icharate.Kernel.basics]
hDiamond [constructor, in Icharate.Kernel.basics]
hole [constructor, in Icharate.Kernel.basics]
Houda [constructor, in Icharate.Examples.polEx]
hres [constructor, in Icharate.Kernel.basics]
hyp [constructor, in Icharate.Kernel.basics]
hyps [constructor, in Icharate.Kernel.lambda_bruijn]
I
I [inductive, in Icharate.Examples.polEx]I [inductive, in Icharate.Examples.medialEx]
I [inductive, in Icharate.Examples.dep_ex]
I [inductive, in Icharate.Examples.ex1]
I [inductive, in Icharate.Examples.ex1s]
I [projection, in Icharate.Kernel.semLex]
ignore [constructor, in Icharate.Examples.polEx]
ignore [constructor, in Icharate.Examples.medialEx]
ignore [constructor, in Icharate.Examples.ex1]
ignore [constructor, in Icharate.Examples.ex1s]
IMPL [constructor, in Icharate.Kernel.logic_const]
incDiam [definition, in Icharate.Kernel.struct_ex]
incDiamImgInv [lemma, in Icharate.Kernel.struct_ex]
incDiam_Inv [lemma, in Icharate.Kernel.struct_ex]
incDiam_rw [definition, in Icharate.Kernel.struct_ex]
incl_distinct_permut [lemma, in Icharate.Lib.listAux]
ind_permu_to_eqmset [lemma, in Icharate.Lib.permutation]
intent [axiom, in Icharate.Kernel.lambda_coq]
intention [constructor, in Icharate.Kernel.lambda_bruijn]
interp_coq [library]
in_extension_right [constructor, in Icharate.Kernel.basics]
in_extension_rule [constructor, in Icharate.Kernel.basics]
in_extension [inductive, in Icharate.Kernel.basics]
in_isLeaf [lemma, in Icharate.Kernel.basics]
isIncl [definition, in Icharate.Lib.listAux]
isIncluded [definition, in Icharate.Kernel.basics]
isIncluded_to_isIncl [lemma, in Icharate.Kernel.basics]
isIncl_app [lemma, in Icharate.Lib.listAux]
isIncl_in [lemma, in Icharate.Lib.listAux]
isLeaf [definition, in Icharate.Kernel.basics]
isLeaf_dec_com [definition, in Icharate.Kernel.basics]
isLeaf_dec [definition, in Icharate.Kernel.basics]
isLeaf_in [lemma, in Icharate.Kernel.basics]
isStrictSubTerm [inductive, in Icharate.Kernel.lambda_reduction]
isSubTerm [inductive, in Icharate.Kernel.lambda_reduction]
isWellFormed [definition, in Icharate.Kernel.lambda_bruijn]
isWellFormedBind [lemma, in Icharate.Kernel.lambda_bruijn]
isWellFormedBindN [lemma, in Icharate.Kernel.lambda_bruijn]
isWellFormedN [definition, in Icharate.Kernel.lambda_bruijn]
isWellFormedSubst [lemma, in Icharate.Kernel.lambda_bruijn]
isWellTyped [inductive, in Icharate.Kernel.lambda_bruijn]
isWellTyped_lex [definition, in Icharate.Kernel.semLex]
isWellTyped_pairs [definition, in Icharate.Kernel.semLex]
isWFStrictSub [lemma, in Icharate.Kernel.lambda_reduction]
is_sub_cont [inductive, in Icharate.Kernel.basics]
I_syn [projection, in Icharate.Kernel.natDedGram]
J
J [inductive, in Icharate.Examples.polEx]J [inductive, in Icharate.Examples.medialEx]
J [inductive, in Icharate.Examples.dep_ex]
J [inductive, in Icharate.Examples.ex1]
J [inductive, in Icharate.Examples.ex1s]
J [projection, in Icharate.Kernel.semLex]
J_syn [projection, in Icharate.Kernel.natDedGram]
K
KDiam [definition, in Icharate.Kernel.struct_ex]KDiamImgInv [lemma, in Icharate.Kernel.struct_ex]
KDiam_Inv [lemma, in Icharate.Kernel.struct_ex]
KDiam_rw [lemma, in Icharate.Kernel.struct_ex]
K2Diam [definition, in Icharate.Kernel.struct_ex]
K2DiamImgInv [lemma, in Icharate.Kernel.struct_ex]
K2Diam_Inv [lemma, in Icharate.Kernel.struct_ex]
K2Diam_rw [lemma, in Icharate.Kernel.struct_ex]
K2Diam_ws [lemma, in Icharate.Kernel.struct_ex]
L
la [constructor, in Icharate.Examples.polEx]la [constructor, in Icharate.Examples.ex1]
la [constructor, in Icharate.Examples.ex1s]
lambdaAbs [definition, in Icharate.Kernel.lambda_bruijn]
lambdaBind [definition, in Icharate.Kernel.lambda_bruijn]
lambdaSubN [definition, in Icharate.Kernel.lambda_bruijn]
lambda_morphism.subst_X_by_Y [variable, in Icharate.Kernel.final_sem]
lambda_morphism.typeY [variable, in Icharate.Kernel.final_sem]
lambda_morphism.typeX [variable, in Icharate.Kernel.final_sem]
lambda_morphism.Y [variable, in Icharate.Kernel.final_sem]
lambda_morphism.X [variable, in Icharate.Kernel.final_sem]
lambda_morphism [section, in Icharate.Kernel.final_sem]
lambda_terms [inductive, in Icharate.Kernel.lambda_bruijn]
lambda_coq [library]
lambda_reduction [library]
lambda_bruijn [library]
lambSub [definition, in Icharate.Kernel.lambda_bruijn]
LBack [constructor, in Icharate.Kernel.sequent]
LBox [constructor, in Icharate.Kernel.sequent]
LDiam [constructor, in Icharate.Kernel.sequent]
LDot [constructor, in Icharate.Kernel.sequent]
leftLinear [definition, in Icharate.Kernel.struct_props]
leftLinearSahlqvist [definition, in Icharate.Kernel.struct_props]
leftLinear_par_replace [definition, in Icharate.Kernel.struct_props]
leftLinear_Diam [lemma, in Icharate.Kernel.struct_props]
leftLinear_Com2 [lemma, in Icharate.Kernel.struct_props]
leftLinear_Com1 [lemma, in Icharate.Kernel.struct_props]
lengthW [definition, in Icharate.Tacs.tacticsDed]
length_app [lemma, in Icharate.Lib.permutation]
lex [definition, in Icharate.Examples.polEx]
lex [definition, in Icharate.Examples.medialEx]
lex [definition, in Icharate.Examples.dep_ex]
lex [definition, in Icharate.Examples.ex1]
lex [definition, in Icharate.Examples.ex1s]
lex [projection, in Icharate.Kernel.semLex]
lexic [projection, in Icharate.Kernel.semLex]
lexicon [record, in Icharate.Kernel.semLex]
lexic_syn [projection, in Icharate.Kernel.natDedGram]
lex_syn [projection, in Icharate.Kernel.natDedGram]
lex_opaq [definition, in Icharate.Examples.ex1]
lex1 [definition, in Icharate.Examples.polEx]
lex1 [definition, in Icharate.Examples.medialEx]
lex1 [definition, in Icharate.Examples.dep_ex]
lex1 [definition, in Icharate.Examples.ex1]
lex1' [definition, in Icharate.Examples.polEx]
lex1' [definition, in Icharate.Examples.ex1]
lex2 [definition, in Icharate.Examples.ex1s]
lift_wf [lemma, in Icharate.Kernel.lambda_bruijn]
lift_lambda [definition, in Icharate.Kernel.lambda_bruijn]
likes [constructor, in Icharate.Examples.dep_ex]
linear [definition, in Icharate.Kernel.struct_props]
linearDiam [definition, in Icharate.Kernel.struct_props]
linearPolarity [lemma, in Icharate.Meta.polarity]
linearTocondStruct [lemma, in Icharate.Meta.unaries]
linear_permut [lemma, in Icharate.Kernel.struct_props]
linear_pol [lemma, in Icharate.Tacs.polTac]
linear_ext [definition, in Icharate.Tacs.polTac]
listAux [library]
listT [inductive, in Icharate.Kernel.lambda_coq]
logic_cst [inductive, in Icharate.Kernel.logic_const]
logic_const [library]
lP [constructor, in Icharate.Tacs.tacticsDed]
LSlash [constructor, in Icharate.Kernel.sequent]
L1 [definition, in Icharate.Kernel.struct_ex]
L1ImgInv [lemma, in Icharate.Kernel.struct_ex]
L1_Inv [lemma, in Icharate.Kernel.struct_ex]
L1_rw [lemma, in Icharate.Kernel.struct_ex]
L2 [definition, in Icharate.Kernel.struct_ex]
L2ImgInv [lemma, in Icharate.Kernel.struct_ex]
L2_Inv [lemma, in Icharate.Kernel.struct_ex]
L2_rw [lemma, in Icharate.Kernel.struct_ex]
M
Main [section, in Icharate.Kernel.natDed]Main.A [variable, in Icharate.Kernel.natDed]
Main.eqdecI [variable, in Icharate.Kernel.natDed]
Main.eqdecJ [variable, in Icharate.Kernel.natDed]
Main.I [variable, in Icharate.Kernel.natDed]
Main.J [variable, in Icharate.Kernel.natDed]
Main.R [variable, in Icharate.Kernel.natDed]
Main.W [variable, in Icharate.Kernel.natDed]
map [definition, in Icharate.Examples.ex1s]
map [projection, in Icharate.Kernel.semLex]
mapExt [definition, in Icharate.Kernel.lambda_bruijn]
map_permut [lemma, in Icharate.Lib.permutation]
map_app [lemma, in Icharate.Lib.permutation]
map_length [lemma, in Icharate.Lib.listAux]
Marie [constructor, in Icharate.Examples.medialEx]
Mary [constructor, in Icharate.Examples.dep_ex]
matches [inductive, in Icharate.Kernel.basics]
matches_inv_Diam [definition, in Icharate.Kernel.basics]
matches_inv_Comma [definition, in Icharate.Kernel.basics]
matches_inv_form [definition, in Icharate.Kernel.basics]
match_strip [lemma, in Icharate.Kernel.basics]
MA1 [definition, in Icharate.Kernel.struct_ex]
MA1ImgInv [lemma, in Icharate.Kernel.struct_ex]
MA1_Inv [lemma, in Icharate.Kernel.struct_ex]
MA1_rw [lemma, in Icharate.Kernel.struct_ex]
MA2 [definition, in Icharate.Kernel.struct_ex]
MA2Diam [definition, in Icharate.Kernel.struct_ex]
MA2DiamImgInv [lemma, in Icharate.Kernel.struct_ex]
MA2DiamRep [definition, in Icharate.Meta.unbounDep]
MA2Diam_Inv [lemma, in Icharate.Kernel.struct_ex]
MA2Diam_rw [lemma, in Icharate.Kernel.struct_ex]
MA2ImgInv [lemma, in Icharate.Kernel.struct_ex]
MA2_Inv [lemma, in Icharate.Kernel.struct_ex]
MA2_rw [lemma, in Icharate.Kernel.struct_ex]
MC [definition, in Icharate.Kernel.struct_ex]
MCImgInv [lemma, in Icharate.Kernel.struct_ex]
MC_Inv [lemma, in Icharate.Kernel.struct_ex]
MC_rw [lemma, in Icharate.Kernel.struct_ex]
medialEx [library]
medialExtraction [definition, in Icharate.Meta.medialExtraction]
medialExtraction [library]
medialMeta [section, in Icharate.Meta.medialExtraction]
medialMeta.A [variable, in Icharate.Meta.medialExtraction]
medialMeta.eqdecI [variable, in Icharate.Meta.medialExtraction]
medialMeta.eqdecJ [variable, in Icharate.Meta.medialExtraction]
medialMeta.ext [variable, in Icharate.Meta.medialExtraction]
medialMeta.i [variable, in Icharate.Meta.medialExtraction]
medialMeta.I [variable, in Icharate.Meta.medialExtraction]
medialMeta.j [variable, in Icharate.Meta.medialExtraction]
medialMeta.J [variable, in Icharate.Meta.medialExtraction]
medialMeta.MA_ij [variable, in Icharate.Meta.medialExtraction]
medialMeta.MP_ij [variable, in Icharate.Meta.medialExtraction]
medialMeta.W [variable, in Icharate.Meta.medialExtraction]
mixed_composition_Geach [definition, in Icharate.Meta.derivedRulesNatDed]
mixed_composition_Slash [definition, in Icharate.Meta.derivedRulesNatDed]
mixed_composition_Back [definition, in Icharate.Meta.derivedRulesNatDed]
mk_gramS [constructor, in Icharate.Kernel.natDedGram]
mk_lexS [constructor, in Icharate.Kernel.natDedGram]
mk_gram [constructor, in Icharate.Kernel.semLex]
mk_lex [constructor, in Icharate.Kernel.semLex]
MonoLeftNRu [definition, in Icharate.Meta.derivedRulesNatDed]
MonoRightNRu [definition, in Icharate.Meta.derivedRulesNatDed]
MP [definition, in Icharate.Kernel.struct_ex]
MPDiam [definition, in Icharate.Kernel.struct_ex]
MPDiamImgInv [lemma, in Icharate.Kernel.struct_ex]
MPDiam_Inv [lemma, in Icharate.Kernel.struct_ex]
MPDiam_rw [lemma, in Icharate.Kernel.struct_ex]
MPImgInv [lemma, in Icharate.Kernel.struct_ex]
MP_Inv [lemma, in Icharate.Kernel.struct_ex]
MP_rw [lemma, in Icharate.Kernel.struct_ex]
MP1Diam [definition, in Icharate.Kernel.struct_ex]
MP1DiamImgInv [lemma, in Icharate.Kernel.struct_ex]
MP1Diam_Inv [lemma, in Icharate.Kernel.struct_ex]
MP1Diam_rw [lemma, in Icharate.Kernel.struct_ex]
MP2Diam [definition, in Icharate.Kernel.struct_ex]
MP2DiamImgInv [lemma, in Icharate.Kernel.struct_ex]
MP2Diam_Inv [lemma, in Icharate.Kernel.struct_ex]
MP2Diam_rw [lemma, in Icharate.Kernel.struct_ex]
multiplicity_one_distinct [lemma, in Icharate.Lib.listAux]
multiplicity_0_notIn [lemma, in Icharate.Lib.listAux]
mult_add_somewhere2 [lemma, in Icharate.Lib.permutation]
mult_add_somewhere1 [lemma, in Icharate.Lib.permutation]
mult_In [lemma, in Icharate.Lib.permutation]
mult_app [lemma, in Icharate.Lib.permutation]
my_contW [definition, in Icharate.Examples.medialEx]
my_contextW [definition, in Icharate.Examples.dep_ex]
my_fragment [definition, in Icharate.Examples.dep_ex]
m1 [constructor, in Icharate.Examples.medialEx]
m1 [constructor, in Icharate.Examples.dep_ex]
m2 [constructor, in Icharate.Examples.medialEx]
m2 [constructor, in Icharate.Examples.dep_ex]
N
n [constructor, in Icharate.Examples.polEx]n [constructor, in Icharate.Examples.medialEx]
n [constructor, in Icharate.Examples.dep_ex]
n [constructor, in Icharate.Examples.ex1]
n [constructor, in Icharate.Examples.ex1s]
natded [inductive, in Icharate.Kernel.natDed]
natDed [library]
natDedGram [library]
natdedNRep [definition, in Icharate.Meta.derivedRulesNatDed]
natDedSeq [section, in Icharate.Meta.seqNatDed]
natDedSeq.A [variable, in Icharate.Meta.seqNatDed]
natDedSeq.eqDecI [variable, in Icharate.Meta.seqNatDed]
natDedSeq.eqDecJ [variable, in Icharate.Meta.seqNatDed]
natDedSeq.I [variable, in Icharate.Meta.seqNatDed]
natDedSeq.J [variable, in Icharate.Meta.seqNatDed]
natDedSeq.W [variable, in Icharate.Meta.seqNatDed]
natDedToSeq [definition, in Icharate.Meta.seqNatDed]
natded_trans [definition, in Icharate.Meta.derivedRulesNatDed]
natded0 [definition, in Icharate.Kernel.natDed]
nf_deriv1 [definition, in Icharate.Examples.ex1s]
nilT [constructor, in Icharate.Kernel.lambda_coq]
nil_trans [constructor, in Icharate.Kernel.lambda_coq]
NL [constructor, in Icharate.Kernel.basics]
noHyps [definition, in Icharate.Examples.ex1s]
noInter [definition, in Icharate.Lib.listAux]
noIntersection [definition, in Icharate.Kernel.basics]
noIntersectionLeaf [lemma, in Icharate.Kernel.basics]
noInter_pattern_to_list [lemma, in Icharate.Kernel.basics]
noInter_app [lemma, in Icharate.Lib.listAux]
NoneT [constructor, in Icharate.Kernel.lambda_coq]
noRep [constructor, in Icharate.Meta.derivedRulesNatDed]
normal [constructor, in Icharate.Kernel.final_sem]
normalForm [definition, in Icharate.Kernel.lambda_reduction]
normalFormExtr [lemma, in Icharate.Kernel.lambda_reduction]
notations [library]
notLeaf [definition, in Icharate.Kernel.struct_props]
notWellFormedNum [lemma, in Icharate.Kernel.lambda_bruijn]
no_holes [lemma, in Icharate.Kernel.basics]
no_hyps_inside [definition, in Icharate.Kernel.lambda_bruijn]
np [constructor, in Icharate.Examples.polEx]
np [constructor, in Icharate.Examples.medialEx]
np [constructor, in Icharate.Examples.dep_ex]
np [constructor, in Icharate.Examples.ex1]
np [constructor, in Icharate.Examples.ex1s]
nth_error_T [definition, in Icharate.Kernel.lambda_coq]
nth_flatten_leaf [lemma, in Icharate.Kernel.basics]
nth_add3 [lemma, in Icharate.Kernel.lambda_bruijn]
nth_add2 [lemma, in Icharate.Kernel.lambda_bruijn]
nth_add1 [lemma, in Icharate.Kernel.lambda_bruijn]
nth_error_scd_app [lemma, in Icharate.Lib.listAux]
nth_error_fst_app [lemma, in Icharate.Lib.listAux]
nth_error_app [lemma, in Icharate.Lib.listAux]
nth_error_some_length [lemma, in Icharate.Lib.listAux]
nth_error_length [lemma, in Icharate.Lib.listAux]
nth_sup_length [lemma, in Icharate.Lib.listAux]
nth_map [lemma, in Icharate.Lib.listAux]
num [constructor, in Icharate.Kernel.lambda_bruijn]
O
objectLift [definition, in Icharate.Meta.derivedRulesNatDed]obj1 [constructor, in Icharate.Kernel.lambda_coq]
oneW [constructor, in Icharate.Tacs.tacticsDed]
one_type [lemma, in Icharate.Kernel.lambda_bruijn]
optionT [inductive, in Icharate.Kernel.lambda_coq]
op_all_permut [lemma, in Icharate.Lib.permutation]
op_all_app [lemma, in Icharate.Lib.permutation]
op_all [definition, in Icharate.Lib.permutation]
OR [constructor, in Icharate.Kernel.logic_const]
P
P [definition, in Icharate.Kernel.struct_ex]par_replace_to_fill [definition, in Icharate.Kernel.basics]
par_replaceDiamond [constructor, in Icharate.Kernel.basics]
par_replaceBin [constructor, in Icharate.Kernel.basics]
par_root [constructor, in Icharate.Kernel.basics]
par_zero [constructor, in Icharate.Kernel.basics]
par_replace [inductive, in Icharate.Kernel.basics]
path [inductive, in Icharate.Tacs.tacticsDed]
pcomma [constructor, in Icharate.Kernel.basics]
pdiam [constructor, in Icharate.Kernel.basics]
perm [section, in Icharate.Lib.permutation]
permt [section, in Icharate.Lib.listAux]
permt.A [variable, in Icharate.Lib.listAux]
permt.decA [variable, in Icharate.Lib.listAux]
permut [inductive, in Icharate.Lib.permutation]
Permutation [definition, in Icharate.Meta.derivedRulesNatDed]
permutation [library]
permutation_add' [lemma, in Icharate.Lib.permutation]
permutation_uncons [lemma, in Icharate.Lib.permutation]
permutation_nil [lemma, in Icharate.Lib.permutation]
Permutation2 [definition, in Icharate.Meta.derivedRulesNatDed]
permut_add_a [lemma, in Icharate.Lib.permutation]
permut_app_same_l [lemma, in Icharate.Lib.permutation]
permut_sym [lemma, in Icharate.Lib.permutation]
permut_app_com [lemma, in Icharate.Lib.permutation]
permut_nil2 [lemma, in Icharate.Lib.permutation]
permut_nil1 [lemma, in Icharate.Lib.permutation]
permut_length [lemma, in Icharate.Lib.permutation]
permut_sub_cont [lemma, in Icharate.Kernel.apply_rule_props]
permut_same_pol [lemma, in Icharate.Meta.polarity]
permut_extract [lemma, in Icharate.Lib.listAux]
perm_trans [constructor, in Icharate.Lib.permutation]
perm_app [constructor, in Icharate.Lib.permutation]
perm_cons [constructor, in Icharate.Lib.permutation]
perm_refl [constructor, in Icharate.Lib.permutation]
perm.A [variable, in Icharate.Lib.permutation]
perm.B [variable, in Icharate.Lib.permutation]
perm.decA [variable, in Icharate.Lib.permutation]
perm.op_permut.op_assoc [variable, in Icharate.Lib.permutation]
perm.op_permut.a_neutral_op [variable, in Icharate.Lib.permutation]
perm.op_permut.op_com [variable, in Icharate.Lib.permutation]
perm.op_permut.a_neutral [variable, in Icharate.Lib.permutation]
perm.op_permut.op [variable, in Icharate.Lib.permutation]
perm.op_permut [section, in Icharate.Lib.permutation]
Peter [constructor, in Icharate.Examples.dep_ex]
PImgInv [lemma, in Icharate.Kernel.struct_ex]
piRed1 [constructor, in Icharate.Kernel.lambda_reduction]
piRed2 [constructor, in Icharate.Kernel.lambda_reduction]
pi1 [constructor, in Icharate.Kernel.lambda_bruijn]
pi1Red [constructor, in Icharate.Kernel.lambda_reduction]
pi2 [constructor, in Icharate.Kernel.lambda_bruijn]
pi2Red [constructor, in Icharate.Kernel.lambda_reduction]
pol [section, in Icharate.Meta.polarity]
polarity [library]
polarityDed [lemma, in Icharate.Meta.polarity]
polarityRef [lemma, in Icharate.Meta.polarity]
polarityRefDed [lemma, in Icharate.Meta.polarity]
polaritySeq [lemma, in Icharate.Meta.polarity]
polEx [library]
polF [definition, in Icharate.Meta.polarity]
polT [definition, in Icharate.Meta.polarity]
polTac [library]
pol.A [variable, in Icharate.Meta.polarity]
pol.eqdecA [variable, in Icharate.Meta.polarity]
pol.eqdecI [variable, in Icharate.Meta.polarity]
pol.eqdecJ [variable, in Icharate.Meta.polarity]
pol.I [variable, in Icharate.Meta.polarity]
pol.J [variable, in Icharate.Meta.polarity]
pol.W [variable, in Icharate.Meta.polarity]
postponing [definition, in Icharate.Meta.derivedRulesNatDed]
preposing [definition, in Icharate.Meta.derivedRulesNatDed]
pretty_printer0 [definition, in Icharate.Kernel.lambda_coq]
pretty_printer [definition, in Icharate.Kernel.interp_coq]
proof_irrelevanceA [lemma, in Icharate.Tacs.struct_tacs]
props [section, in Icharate.Meta.derivedRulesNatDed]
props [section, in Icharate.Kernel.apply_rule_props]
props.A [variable, in Icharate.Meta.derivedRulesNatDed]
props.A [variable, in Icharate.Kernel.apply_rule_props]
props.eqdecI [variable, in Icharate.Meta.derivedRulesNatDed]
props.eqdecJ [variable, in Icharate.Meta.derivedRulesNatDed]
props.ext [variable, in Icharate.Meta.derivedRulesNatDed]
props.I [variable, in Icharate.Meta.derivedRulesNatDed]
props.I [variable, in Icharate.Kernel.apply_rule_props]
props.J [variable, in Icharate.Meta.derivedRulesNatDed]
props.J [variable, in Icharate.Kernel.apply_rule_props]
props.L [section, in Icharate.Meta.derivedRulesNatDed]
props.LP [section, in Icharate.Meta.derivedRulesNatDed]
props.LP.c [variable, in Icharate.Meta.derivedRulesNatDed]
props.LP.L1_c [variable, in Icharate.Meta.derivedRulesNatDed]
props.LP.L2_c [variable, in Icharate.Meta.derivedRulesNatDed]
props.LP.P_c [variable, in Icharate.Meta.derivedRulesNatDed]
props.L.a [variable, in Icharate.Meta.derivedRulesNatDed]
props.L.L1_a [variable, in Icharate.Meta.derivedRulesNatDed]
props.L.L2_a [variable, in Icharate.Meta.derivedRulesNatDed]
props.MC [section, in Icharate.Meta.derivedRulesNatDed]
props.MC.i [variable, in Icharate.Meta.derivedRulesNatDed]
props.MC.j [variable, in Icharate.Meta.derivedRulesNatDed]
props.MC.MC_ij [variable, in Icharate.Meta.derivedRulesNatDed]
props.MP [section, in Icharate.Meta.derivedRulesNatDed]
props.MP.h [variable, in Icharate.Meta.derivedRulesNatDed]
props.MP.MP_hr [variable, in Icharate.Meta.derivedRulesNatDed]
props.MP.r [variable, in Icharate.Meta.derivedRulesNatDed]
props.P [section, in Icharate.Meta.derivedRulesNatDed]
props.P.c [variable, in Icharate.Meta.derivedRulesNatDed]
props.P.p_c [variable, in Icharate.Meta.derivedRulesNatDed]
props.W [variable, in Icharate.Meta.derivedRulesNatDed]
props.W [variable, in Icharate.Kernel.apply_rule_props]
pvar [constructor, in Icharate.Kernel.basics]
P_Inv [lemma, in Icharate.Kernel.struct_ex]
P_rw [lemma, in Icharate.Kernel.struct_ex]
Q
que [constructor, in Icharate.Examples.polEx]que [constructor, in Icharate.Examples.medialEx]
que [constructor, in Icharate.Examples.ex1]
que [constructor, in Icharate.Examples.ex1s]
R
raison [constructor, in Icharate.Examples.polEx]raison [constructor, in Icharate.Examples.ex1]
raison [constructor, in Icharate.Examples.ex1s]
RBack [constructor, in Icharate.Kernel.sequent]
RBox [constructor, in Icharate.Kernel.sequent]
RDiam [constructor, in Icharate.Kernel.sequent]
RDot [constructor, in Icharate.Kernel.sequent]
redexAppl [lemma, in Icharate.Kernel.lambda_reduction]
redexDebox [lemma, in Icharate.Kernel.lambda_reduction]
redexDediam [lemma, in Icharate.Kernel.lambda_reduction]
redexNF [lemma, in Icharate.Kernel.lambda_reduction]
redexPi1 [lemma, in Icharate.Kernel.lambda_reduction]
redexPi2 [lemma, in Icharate.Kernel.lambda_reduction]
reduceAll [definition, in Icharate.Kernel.lambda_reduction]
reduceAllBeta [lemma, in Icharate.Kernel.lambda_reduction]
reduceAllWellFound [lemma, in Icharate.Kernel.lambda_reduction]
reduceTo [inductive, in Icharate.Kernel.natDedGram]
reduce1 [constructor, in Icharate.Kernel.natDedGram]
repDistribute [definition, in Icharate.Meta.crossDep]
repExtnatDed [definition, in Icharate.Meta.derivedRulesNatDed]
replace [inductive, in Icharate.Kernel.basics]
replaceDB [lemma, in Icharate.Meta.unaries]
replaceDiamond [constructor, in Icharate.Kernel.basics]
replaceExtMonoLeft [definition, in Icharate.Meta.derivedRulesNatDed]
replaceExtMonoRight [definition, in Icharate.Meta.derivedRulesNatDed]
replaceLeft [constructor, in Icharate.Kernel.basics]
replaceNatDed [definition, in Icharate.Meta.seqNatDed]
replaceNTimes [inductive, in Icharate.Meta.derivedRulesNatDed]
replaceNTimesExt [inductive, in Icharate.Meta.derivedRulesNatDed]
replaceParCom [definition, in Icharate.Kernel.basics]
replaceParDiam [definition, in Icharate.Kernel.basics]
replacePolarity [lemma, in Icharate.Meta.polarity]
replaceProp [definition, in Icharate.Kernel.basics]
replaceRight [constructor, in Icharate.Kernel.basics]
replaceRoot [constructor, in Icharate.Kernel.basics]
replaceStruct [lemma, in Icharate.Meta.polarity]
replaceTermByTerm [definition, in Icharate.Tacs.tacticsDed]
replace_to_par [definition, in Icharate.Kernel.basics]
replace_props [section, in Icharate.Kernel.basics]
replace_to_zfill [definition, in Icharate.Kernel.basics]
replExtMono [definition, in Icharate.Meta.derivedRulesNatDed]
replExtTrans [definition, in Icharate.Meta.derivedRulesNatDed]
replNPermut [definition, in Icharate.Meta.derivedRulesNatDed]
repRu [constructor, in Icharate.Meta.derivedRulesNatDed]
repToParRep [definition, in Icharate.Kernel.basics]
repTransform [definition, in Icharate.Meta.crossDep]
rep1 [constructor, in Icharate.Meta.derivedRulesNatDed]
rep2 [constructor, in Icharate.Meta.derivedRulesNatDed]
res [constructor, in Icharate.Kernel.basics]
resource [inductive, in Icharate.Kernel.basics]
ress [constructor, in Icharate.Kernel.lambda_bruijn]
restructuring_r [definition, in Icharate.Meta.derivedRulesNatDed]
restructuring_l [definition, in Icharate.Meta.derivedRulesNatDed]
rightLinear [definition, in Icharate.Kernel.struct_props]
rP [constructor, in Icharate.Tacs.tacticsDed]
RSlash [constructor, in Icharate.Kernel.sequent]
rstruct_replaceRight [constructor, in Icharate.Kernel.basics]
rule_pattern [inductive, in Icharate.Kernel.basics]
S
s [constructor, in Icharate.Examples.polEx]s [constructor, in Icharate.Examples.medialEx]
s [constructor, in Icharate.Examples.dep_ex]
s [constructor, in Icharate.Examples.ex1]
s [constructor, in Icharate.Examples.ex1s]
sameShapeCom [definition, in Icharate.Kernel.basics]
sameShapeDiam [definition, in Icharate.Kernel.basics]
sameT [constructor, in Icharate.Kernel.lambda_reduction]
same_type_after_subst [lemma, in Icharate.Kernel.final_sem]
same_type [definition, in Icharate.Kernel.final_sem]
same_shape_par_replace [lemma, in Icharate.Kernel.basics]
same_shape_SubCont [lemma, in Icharate.Kernel.basics]
same_shape_diam [constructor, in Icharate.Kernel.basics]
same_shape_comma [constructor, in Icharate.Kernel.basics]
same_shape_leaf [constructor, in Icharate.Kernel.basics]
same_shape [inductive, in Icharate.Kernel.basics]
same_shape_left_linear [definition, in Icharate.Kernel.struct_props]
semantic [section, in Icharate.Kernel.final_sem]
semantic [section, in Icharate.Kernel.derivSem]
semanticTerm [definition, in Icharate.Kernel.derivSem]
semantic.A [variable, in Icharate.Kernel.final_sem]
semantic.A [variable, in Icharate.Kernel.derivSem]
semantic.eqDecI [variable, in Icharate.Kernel.derivSem]
semantic.eqDecJ [variable, in Icharate.Kernel.derivSem]
semantic.ext [variable, in Icharate.Kernel.derivSem]
semantic.I [variable, in Icharate.Kernel.final_sem]
semantic.I [variable, in Icharate.Kernel.derivSem]
semantic.J [variable, in Icharate.Kernel.final_sem]
semantic.J [variable, in Icharate.Kernel.derivSem]
semantic.lexi [variable, in Icharate.Kernel.final_sem]
semantic.map [variable, in Icharate.Kernel.final_sem]
semantic.map [variable, in Icharate.Kernel.derivSem]
semantic.W [variable, in Icharate.Kernel.final_sem]
semantic.W [variable, in Icharate.Kernel.derivSem]
semLex [library]
semType [inductive, in Icharate.Kernel.lambda_bruijn]
semW [axiom, in Icharate.Kernel.interp_coq]
semWellDefined [lemma, in Icharate.Kernel.derivSem]
sem_wt [lemma, in Icharate.Kernel.final_sem]
seqNatDed [library]
seqToNatded [definition, in Icharate.Meta.seqNatDed]
sequent [library]
setSynLex [definition, in Icharate.Kernel.natDedGram]
setTypeLog [definition, in Icharate.Kernel.logic_const]
set_syn_sem_Lex [definition, in Icharate.Kernel.semLex]
simplBetaToRefTrans [lemma, in Icharate.Kernel.lambda_reduction]
simple_cut_rule [definition, in Icharate.Meta.derivedRulesNatDed]
Slash [constructor, in Icharate.Kernel.basics]
SlashE [constructor, in Icharate.Kernel.natDed]
SlashI [constructor, in Icharate.Kernel.natDed]
Slash_antitonicity [definition, in Icharate.Meta.derivedRulesNatDed]
Slash_lifting [definition, in Icharate.Meta.derivedRulesNatDed]
SomeT [constructor, in Icharate.Kernel.lambda_coq]
ssubAbs [constructor, in Icharate.Kernel.lambda_reduction]
ssubAppl1 [constructor, in Icharate.Kernel.lambda_reduction]
ssubAppl2 [constructor, in Icharate.Kernel.lambda_reduction]
ssubBox [constructor, in Icharate.Kernel.lambda_reduction]
ssubDebox [constructor, in Icharate.Kernel.lambda_reduction]
ssubDediam [constructor, in Icharate.Kernel.lambda_reduction]
ssubDiam [constructor, in Icharate.Kernel.lambda_reduction]
ssubPi1 [constructor, in Icharate.Kernel.lambda_reduction]
ssubPi2 [constructor, in Icharate.Kernel.lambda_reduction]
ssubTwoL1 [constructor, in Icharate.Kernel.lambda_reduction]
ssubTwoL2 [constructor, in Icharate.Kernel.lambda_reduction]
strip_match [lemma, in Icharate.Kernel.basics]
structPol [definition, in Icharate.Meta.polarity]
StructR [constructor, in Icharate.Kernel.sequent]
structRepDB [lemma, in Icharate.Meta.unaries]
structrule [definition, in Icharate.Kernel.basics]
StructRule [constructor, in Icharate.Kernel.natDed]
structrule_subst_commute [definition, in Icharate.Kernel.basics]
Structrule' [definition, in Icharate.Kernel.natDed]
struct_replace_to_zfill [definition, in Icharate.Kernel.basics]
struct_replace_as_zfill [definition, in Icharate.Kernel.basics]
struct_replaceDiamond [constructor, in Icharate.Kernel.basics]
struct_replaceLeft [constructor, in Icharate.Kernel.basics]
struct_replaceRoot [constructor, in Icharate.Kernel.basics]
struct_replace [inductive, in Icharate.Kernel.basics]
struct_tacs [library]
struct_ex [library]
struct_props [library]
subAbs [constructor, in Icharate.Kernel.lambda_reduction]
subAppl1 [constructor, in Icharate.Kernel.lambda_reduction]
subAppl2 [constructor, in Icharate.Kernel.lambda_reduction]
subBox [constructor, in Icharate.Kernel.lambda_reduction]
subCont_length [lemma, in Icharate.Kernel.basics]
subCont_same_shape [lemma, in Icharate.Kernel.basics]
subDebox [constructor, in Icharate.Kernel.lambda_reduction]
subDediam [constructor, in Icharate.Kernel.lambda_reduction]
subDiam [constructor, in Icharate.Kernel.lambda_reduction]
subPi1 [constructor, in Icharate.Kernel.lambda_reduction]
subPi2 [constructor, in Icharate.Kernel.lambda_reduction]
substLamb [definition, in Icharate.Kernel.lambda_reduction]
substVar [definition, in Icharate.Kernel.lambda_reduction]
subTwoL1 [constructor, in Icharate.Kernel.lambda_reduction]
subTwoL2 [constructor, in Icharate.Kernel.lambda_reduction]
sub_diam [constructor, in Icharate.Kernel.basics]
sub_right [constructor, in Icharate.Kernel.basics]
sub_left [constructor, in Icharate.Kernel.basics]
sub_all [constructor, in Icharate.Kernel.basics]
sub_eq_strict [lemma, in Icharate.Kernel.lambda_reduction]
sub_cont_pol [lemma, in Icharate.Meta.polarity]
sum_diff_leaves [definition, in Icharate.Meta.unaries]
sum_all [definition, in Icharate.Lib.listAux]
synGram [record, in Icharate.Kernel.natDedGram]
synLexicon [record, in Icharate.Kernel.natDedGram]
syntaxNatDed [section, in Icharate.Kernel.natDedGram]
syntaxNatDed.A [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.eqdecI [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.eqdecJ [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.ext [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.I [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.J [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.lexSyn [variable, in Icharate.Kernel.natDedGram]
syntaxNatDed.W [variable, in Icharate.Kernel.natDedGram]
syn_sem_gram [record, in Icharate.Kernel.semLex]
S_combinator [definition, in Icharate.Meta.derivedRulesNatDed]
T
t [constructor, in Icharate.Kernel.lambda_bruijn]tacticsDed [library]
tacticsSeq [library]
TDiamond [constructor, in Icharate.Kernel.basics]
thinks [constructor, in Icharate.Examples.dep_ex]
to_coq.W [variable, in Icharate.Kernel.interp_coq]
to_coq [section, in Icharate.Kernel.interp_coq]
trans [definition, in Icharate.Kernel.final_sem]
transformCont [definition, in Icharate.Meta.crossDep]
translate [definition, in Icharate.Kernel.final_sem]
trans_lamb0 [definition, in Icharate.Kernel.lambda_coq]
trans_lamb [definition, in Icharate.Kernel.lambda_coq]
trans_env_nth [definition, in Icharate.Kernel.lambda_coq]
trans_env [inductive, in Icharate.Kernel.lambda_coq]
trans_type [definition, in Icharate.Kernel.lambda_coq]
treeDeri [definition, in Icharate.Examples.medialEx]
treeDeriv [definition, in Icharate.Examples.dep_ex]
twoL [constructor, in Icharate.Kernel.lambda_bruijn]
twoLRed1 [constructor, in Icharate.Kernel.lambda_reduction]
twoLRed2 [constructor, in Icharate.Kernel.lambda_reduction]
typeAbs [constructor, in Icharate.Kernel.lambda_bruijn]
typeAppl [constructor, in Icharate.Kernel.lambda_bruijn]
typeBox [constructor, in Icharate.Kernel.lambda_bruijn]
typeDebox [constructor, in Icharate.Kernel.lambda_bruijn]
typeDediam [constructor, in Icharate.Kernel.lambda_bruijn]
typeDiam [constructor, in Icharate.Kernel.lambda_bruijn]
typeHyps [constructor, in Icharate.Kernel.lambda_bruijn]
typeNum [constructor, in Icharate.Kernel.lambda_bruijn]
typePi1 [constructor, in Icharate.Kernel.lambda_bruijn]
typePi2 [constructor, in Icharate.Kernel.lambda_bruijn]
typeTwoL [constructor, in Icharate.Kernel.lambda_bruijn]
typeVar [constructor, in Icharate.Kernel.lambda_bruijn]
type_obj [inductive, in Icharate.Kernel.lambda_coq]
type_cst [definition, in Icharate.Kernel.final_sem]
type_check_wellTyped [lemma, in Icharate.Kernel.lambda_bruijn]
type_check [definition, in Icharate.Kernel.lambda_bruijn]
U
unaries [section, in Icharate.Meta.unaries]unaries [library]
unaries.A [variable, in Icharate.Meta.unaries]
unaries.decI [variable, in Icharate.Meta.unaries]
unaries.decJ [variable, in Icharate.Meta.unaries]
unaries.I [variable, in Icharate.Meta.unaries]
unaries.J [variable, in Icharate.Meta.unaries]
unaries.W [variable, in Icharate.Meta.unaries]
unboundDep [definition, in Icharate.Meta.unbounDep]
unboundDepend [definition, in Icharate.Meta.unbounDep]
unboundDepend [section, in Icharate.Meta.unbounDep]
unboundDepend.A [variable, in Icharate.Meta.unbounDep]
unboundDepend.eqdecI [variable, in Icharate.Meta.unbounDep]
unboundDepend.eqdecJ [variable, in Icharate.Meta.unbounDep]
unboundDepend.ext [variable, in Icharate.Meta.unbounDep]
unboundDepend.I [variable, in Icharate.Meta.unbounDep]
unboundDepend.J [variable, in Icharate.Meta.unbounDep]
unboundDepend.W [variable, in Icharate.Meta.unbounDep]
unbounDep [library]
up_lambda [definition, in Icharate.Kernel.lambda_bruijn]
W
W [inductive, in Icharate.Examples.polEx]W [inductive, in Icharate.Examples.medialEx]
W [inductive, in Icharate.Examples.dep_ex]
W [inductive, in Icharate.Examples.ex1]
W [inductive, in Icharate.Examples.ex1s]
W [projection, in Icharate.Kernel.semLex]
Wd [constructor, in Icharate.Kernel.natDed]
weakSahlqvist [definition, in Icharate.Kernel.struct_props]
weak_sahlqvist_ext [definition, in Icharate.Kernel.basics]
weak_sahlqvist_rule [definition, in Icharate.Kernel.basics]
wellFLe [lemma, in Icharate.Kernel.lambda_bruijn]
wellFLe1 [lemma, in Icharate.Kernel.lambda_bruijn]
wellFLe2 [lemma, in Icharate.Kernel.lambda_bruijn]
wellFormedUp [lemma, in Icharate.Kernel.lambda_bruijn]
wellFormNSub [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedAbs [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedAppEnv [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedBind [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedFormed [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedSem [lemma, in Icharate.Kernel.derivSem]
wellTypedSub [lemma, in Icharate.Kernel.lambda_bruijn]
wellTypedSubst [lemma, in Icharate.Kernel.lambda_bruijn]
wellTyped_deriv_sem [lemma, in Icharate.Kernel.derivSem]
wellTyped_type_check [lemma, in Icharate.Kernel.lambda_bruijn]
well_typed_no_empty [lemma, in Icharate.Kernel.semLex]
wf_lex [lemma, in Icharate.Examples.ex1s]
whole_sem [definition, in Icharate.Kernel.final_sem]
whom [constructor, in Icharate.Examples.dep_ex]
word [constructor, in Icharate.Kernel.basics]
word_to_lambda [definition, in Icharate.Kernel.final_sem]
word_type [inductive, in Icharate.Kernel.derivSem]
wt [definition, in Icharate.Examples.ex1s]
wt [constructor, in Icharate.Kernel.derivSem]
wt_lex [projection, in Icharate.Kernel.semLex]
W_syn [projection, in Icharate.Kernel.natDedGram]
X
XStructRule [definition, in Icharate.Kernel.natDed]XStructrule' [definition, in Icharate.Kernel.natDed]
Z
zcontext [inductive, in Icharate.Kernel.basics]zcontext_inject [definition, in Icharate.Kernel.basics]
zcontext_inject_aux [definition, in Icharate.Kernel.basics]
zdown [constructor, in Icharate.Kernel.basics]
zfill [definition, in Icharate.Kernel.basics]
zfill_to_struct_replace_0 [definition, in Icharate.Kernel.basics]
zfill_to_replace [definition, in Icharate.Kernel.basics]
zfill_to_replace_0 [definition, in Icharate.Kernel.basics]
zfill_fill [lemma, in Icharate.Kernel.basics]
zfill_fill_0 [lemma, in Icharate.Kernel.basics]
zgraft [definition, in Icharate.Kernel.basics]
zgraft_def [lemma, in Icharate.Kernel.basics]
zleft [constructor, in Icharate.Kernel.basics]
zright [constructor, in Icharate.Kernel.basics]
zroot [constructor, in Icharate.Kernel.basics]
other
% _ (mmg_scope) [notation, in Icharate.Kernel.notations]@ _ (mmg_scope) [notation, in Icharate.Kernel.notations]
>< _ (mmg_scope) [notation, in Icharate.Kernel.notations]
][ _ (mmg_scope) [notation, in Icharate.Kernel.notations]
<> _ (mmg_scope) [notation, in Icharate.Kernel.notations]
[] _ (mmg_scope) [notation, in Icharate.Kernel.notations]
P2 _ (mmg_scope) [notation, in Icharate.Kernel.notations]
P1 _ (mmg_scope) [notation, in Icharate.Kernel.notations]
[[ _ ]]: _ (mmg_scope) [notation, in Icharate.Kernel.notations]
s--> _ (mmg_scope) [notation, in Icharate.Kernel.notations]
_ |*| _ (mmg_scope) [notation, in Icharate.Kernel.notations]
_ --> _ (mmg_scope) [notation, in Icharate.Kernel.notations]
_ { _ _ _ } |-- _ (mmg_scope) [notation, in Icharate.Kernel.natDed]
_ :> _ [notation, in Icharate.Examples.polEx]
_ ;1 _ [notation, in Icharate.Examples.polEx]
_ ,1 _ [notation, in Icharate.Examples.polEx]
_ o1 _ [notation, in Icharate.Examples.polEx]
_ \1 _ [notation, in Icharate.Examples.polEx]
_ /1 _ [notation, in Icharate.Examples.polEx]
_ :> _ [notation, in Icharate.Examples.medialEx]
_ ;1 _ [notation, in Icharate.Examples.medialEx]
_ ,1 _ [notation, in Icharate.Examples.medialEx]
_ o1 _ [notation, in Icharate.Examples.medialEx]
_ \1 _ [notation, in Icharate.Examples.medialEx]
_ /1 _ [notation, in Icharate.Examples.medialEx]
_ {{ _ _ _ _ }} >-> _ [notation, in Icharate.Kernel.natDedGram]
_ :> _ [notation, in Icharate.Examples.dep_ex]
_ ;1 _ [notation, in Icharate.Examples.dep_ex]
_ ,1 _ [notation, in Icharate.Examples.dep_ex]
_ o1 _ [notation, in Icharate.Examples.dep_ex]
_ \1 _ [notation, in Icharate.Examples.dep_ex]
_ /1 _ [notation, in Icharate.Examples.dep_ex]
_ :> _ [notation, in Icharate.Examples.ex1]
_ ;1 _ [notation, in Icharate.Examples.ex1]
_ ,1 _ [notation, in Icharate.Examples.ex1]
_ o1 _ [notation, in Icharate.Examples.ex1]
_ \1 _ [notation, in Icharate.Examples.ex1]
_ /1 _ [notation, in Icharate.Examples.ex1]
_ U _ [notation, in Icharate.Kernel.basics]
_ :> _ [notation, in Icharate.Examples.ex1s]
_ ;1 _ [notation, in Icharate.Examples.ex1s]
_ ,1 _ [notation, in Icharate.Examples.ex1s]
_ o1 _ [notation, in Icharate.Examples.ex1s]
_ \1 _ [notation, in Icharate.Examples.ex1s]
_ /1 _ [notation, in Icharate.Examples.ex1s]
s-> _ [notation, in Icharate.Kernel.lambda_coq]
! _ [notation, in Icharate.Examples.polEx]
! _ [notation, in Icharate.Examples.medialEx]
! _ [notation, in Icharate.Examples.dep_ex]
! _ [notation, in Icharate.Examples.ex1]
! _ [notation, in Icharate.Examples.ex1s]
# _ [notation, in Icharate.Examples.polEx]
# _ [notation, in Icharate.Examples.medialEx]
# _ [notation, in Icharate.Examples.dep_ex]
# _ [notation, in Icharate.Examples.ex1]
# _ [notation, in Icharate.Examples.ex1s]
<>0 _ [notation, in Icharate.Examples.medialEx]
<>0 _ [notation, in Icharate.Examples.dep_ex]
[]0 _ [notation, in Icharate.Examples.medialEx]
[]0 _ [notation, in Icharate.Examples.dep_ex]
|| _ ||: _ >> _ [notation, in Icharate.Kernel.natDedGram]
|| _ ||s: _ >> _ [notation, in Icharate.Kernel.semLex]
Notation Index
other
% _ (mmg_scope) [in Icharate.Kernel.notations]@ _ (mmg_scope) [in Icharate.Kernel.notations]
>< _ (mmg_scope) [in Icharate.Kernel.notations]
][ _ (mmg_scope) [in Icharate.Kernel.notations]
<> _ (mmg_scope) [in Icharate.Kernel.notations]
[] _ (mmg_scope) [in Icharate.Kernel.notations]
P2 _ (mmg_scope) [in Icharate.Kernel.notations]
P1 _ (mmg_scope) [in Icharate.Kernel.notations]
[[ _ ]]: _ (mmg_scope) [in Icharate.Kernel.notations]
s--> _ (mmg_scope) [in Icharate.Kernel.notations]
_ |*| _ (mmg_scope) [in Icharate.Kernel.notations]
_ --> _ (mmg_scope) [in Icharate.Kernel.notations]
_ { _ _ _ } |-- _ (mmg_scope) [in Icharate.Kernel.natDed]
_ :> _ [in Icharate.Examples.polEx]
_ ;1 _ [in Icharate.Examples.polEx]
_ ,1 _ [in Icharate.Examples.polEx]
_ o1 _ [in Icharate.Examples.polEx]
_ \1 _ [in Icharate.Examples.polEx]
_ /1 _ [in Icharate.Examples.polEx]
_ :> _ [in Icharate.Examples.medialEx]
_ ;1 _ [in Icharate.Examples.medialEx]
_ ,1 _ [in Icharate.Examples.medialEx]
_ o1 _ [in Icharate.Examples.medialEx]
_ \1 _ [in Icharate.Examples.medialEx]
_ /1 _ [in Icharate.Examples.medialEx]
_ {{ _ _ _ _ }} >-> _ [in Icharate.Kernel.natDedGram]
_ :> _ [in Icharate.Examples.dep_ex]
_ ;1 _ [in Icharate.Examples.dep_ex]
_ ,1 _ [in Icharate.Examples.dep_ex]
_ o1 _ [in Icharate.Examples.dep_ex]
_ \1 _ [in Icharate.Examples.dep_ex]
_ /1 _ [in Icharate.Examples.dep_ex]
_ :> _ [in Icharate.Examples.ex1]
_ ;1 _ [in Icharate.Examples.ex1]
_ ,1 _ [in Icharate.Examples.ex1]
_ o1 _ [in Icharate.Examples.ex1]
_ \1 _ [in Icharate.Examples.ex1]
_ /1 _ [in Icharate.Examples.ex1]
_ U _ [in Icharate.Kernel.basics]
_ :> _ [in Icharate.Examples.ex1s]
_ ;1 _ [in Icharate.Examples.ex1s]
_ ,1 _ [in Icharate.Examples.ex1s]
_ o1 _ [in Icharate.Examples.ex1s]
_ \1 _ [in Icharate.Examples.ex1s]
_ /1 _ [in Icharate.Examples.ex1s]
s-> _ [in Icharate.Kernel.lambda_coq]
! _ [in Icharate.Examples.polEx]
! _ [in Icharate.Examples.medialEx]
! _ [in Icharate.Examples.dep_ex]
! _ [in Icharate.Examples.ex1]
! _ [in Icharate.Examples.ex1s]
# _ [in Icharate.Examples.polEx]
# _ [in Icharate.Examples.medialEx]
# _ [in Icharate.Examples.dep_ex]
# _ [in Icharate.Examples.ex1]
# _ [in Icharate.Examples.ex1s]
<>0 _ [in Icharate.Examples.medialEx]
<>0 _ [in Icharate.Examples.dep_ex]
[]0 _ [in Icharate.Examples.medialEx]
[]0 _ [in Icharate.Examples.dep_ex]
|| _ ||: _ >> _ [in Icharate.Kernel.natDedGram]
|| _ ||s: _ >> _ [in Icharate.Kernel.semLex]
Variable Index
A
allSem.A [in Icharate.Kernel.lambda_bruijn]allSem.I [in Icharate.Kernel.lambda_bruijn]
allSem.J [in Icharate.Kernel.lambda_bruijn]
allSem.lambdaX.getSemTypeX [in Icharate.Kernel.lambda_bruijn]
allSem.lambdaX.X [in Icharate.Kernel.lambda_bruijn]
allSem.map [in Icharate.Kernel.lambda_bruijn]
B
beta.X [in Icharate.Kernel.lambda_reduction]C
classes.I [in Icharate.Kernel.struct_props]classes.J [in Icharate.Kernel.struct_props]
coq_terms.consts [in Icharate.Kernel.lambda_coq]
coq_terms.getSemTypeX [in Icharate.Kernel.lambda_coq]
coq_terms.X [in Icharate.Kernel.lambda_coq]
cross_dep.R [in Icharate.Meta.crossDep]
cross_dep.eqdecW [in Icharate.Meta.crossDep]
cross_dep.eqdecA [in Icharate.Meta.crossDep]
cross_dep.eqdecJ [in Icharate.Meta.crossDep]
cross_dep.eqdecI [in Icharate.Meta.crossDep]
cross_dep.W [in Icharate.Meta.crossDep]
cross_dep.A [in Icharate.Meta.crossDep]
cross_dep.J [in Icharate.Meta.crossDep]
cross_dep.I [in Icharate.Meta.crossDep]
D
Definitions.Main.formulae_etc.W [in Icharate.Kernel.basics]Definitions.Main.formulae_etc.A [in Icharate.Kernel.basics]
Definitions.Main.I [in Icharate.Kernel.basics]
Definitions.Main.J [in Icharate.Kernel.basics]
Definitions.Main.rep.A [in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.Ru [in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.decJ [in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def.decI [in Icharate.Kernel.basics]
Definitions.Main.rep.W [in Icharate.Kernel.basics]
defs.A [in Icharate.Kernel.sequent]
defs.decI [in Icharate.Kernel.sequent]
defs.decJ [in Icharate.Kernel.sequent]
defs.I [in Icharate.Kernel.sequent]
defs.J [in Icharate.Kernel.sequent]
defs.R [in Icharate.Kernel.sequent]
defs.W [in Icharate.Kernel.sequent]
L
lambda_morphism.subst_X_by_Y [in Icharate.Kernel.final_sem]lambda_morphism.typeY [in Icharate.Kernel.final_sem]
lambda_morphism.typeX [in Icharate.Kernel.final_sem]
lambda_morphism.Y [in Icharate.Kernel.final_sem]
lambda_morphism.X [in Icharate.Kernel.final_sem]
M
Main.A [in Icharate.Kernel.natDed]Main.eqdecI [in Icharate.Kernel.natDed]
Main.eqdecJ [in Icharate.Kernel.natDed]
Main.I [in Icharate.Kernel.natDed]
Main.J [in Icharate.Kernel.natDed]
Main.R [in Icharate.Kernel.natDed]
Main.W [in Icharate.Kernel.natDed]
medialMeta.A [in Icharate.Meta.medialExtraction]
medialMeta.eqdecI [in Icharate.Meta.medialExtraction]
medialMeta.eqdecJ [in Icharate.Meta.medialExtraction]
medialMeta.ext [in Icharate.Meta.medialExtraction]
medialMeta.i [in Icharate.Meta.medialExtraction]
medialMeta.I [in Icharate.Meta.medialExtraction]
medialMeta.j [in Icharate.Meta.medialExtraction]
medialMeta.J [in Icharate.Meta.medialExtraction]
medialMeta.MA_ij [in Icharate.Meta.medialExtraction]
medialMeta.MP_ij [in Icharate.Meta.medialExtraction]
medialMeta.W [in Icharate.Meta.medialExtraction]
N
natDedSeq.A [in Icharate.Meta.seqNatDed]natDedSeq.eqDecI [in Icharate.Meta.seqNatDed]
natDedSeq.eqDecJ [in Icharate.Meta.seqNatDed]
natDedSeq.I [in Icharate.Meta.seqNatDed]
natDedSeq.J [in Icharate.Meta.seqNatDed]
natDedSeq.W [in Icharate.Meta.seqNatDed]
P
permt.A [in Icharate.Lib.listAux]permt.decA [in Icharate.Lib.listAux]
perm.A [in Icharate.Lib.permutation]
perm.B [in Icharate.Lib.permutation]
perm.decA [in Icharate.Lib.permutation]
perm.op_permut.op_assoc [in Icharate.Lib.permutation]
perm.op_permut.a_neutral_op [in Icharate.Lib.permutation]
perm.op_permut.op_com [in Icharate.Lib.permutation]
perm.op_permut.a_neutral [in Icharate.Lib.permutation]
perm.op_permut.op [in Icharate.Lib.permutation]
pol.A [in Icharate.Meta.polarity]
pol.eqdecA [in Icharate.Meta.polarity]
pol.eqdecI [in Icharate.Meta.polarity]
pol.eqdecJ [in Icharate.Meta.polarity]
pol.I [in Icharate.Meta.polarity]
pol.J [in Icharate.Meta.polarity]
pol.W [in Icharate.Meta.polarity]
props.A [in Icharate.Meta.derivedRulesNatDed]
props.A [in Icharate.Kernel.apply_rule_props]
props.eqdecI [in Icharate.Meta.derivedRulesNatDed]
props.eqdecJ [in Icharate.Meta.derivedRulesNatDed]
props.ext [in Icharate.Meta.derivedRulesNatDed]
props.I [in Icharate.Meta.derivedRulesNatDed]
props.I [in Icharate.Kernel.apply_rule_props]
props.J [in Icharate.Meta.derivedRulesNatDed]
props.J [in Icharate.Kernel.apply_rule_props]
props.LP.c [in Icharate.Meta.derivedRulesNatDed]
props.LP.L1_c [in Icharate.Meta.derivedRulesNatDed]
props.LP.L2_c [in Icharate.Meta.derivedRulesNatDed]
props.LP.P_c [in Icharate.Meta.derivedRulesNatDed]
props.L.a [in Icharate.Meta.derivedRulesNatDed]
props.L.L1_a [in Icharate.Meta.derivedRulesNatDed]
props.L.L2_a [in Icharate.Meta.derivedRulesNatDed]
props.MC.i [in Icharate.Meta.derivedRulesNatDed]
props.MC.j [in Icharate.Meta.derivedRulesNatDed]
props.MC.MC_ij [in Icharate.Meta.derivedRulesNatDed]
props.MP.h [in Icharate.Meta.derivedRulesNatDed]
props.MP.MP_hr [in Icharate.Meta.derivedRulesNatDed]
props.MP.r [in Icharate.Meta.derivedRulesNatDed]
props.P.c [in Icharate.Meta.derivedRulesNatDed]
props.P.p_c [in Icharate.Meta.derivedRulesNatDed]
props.W [in Icharate.Meta.derivedRulesNatDed]
props.W [in Icharate.Kernel.apply_rule_props]
S
semantic.A [in Icharate.Kernel.final_sem]semantic.A [in Icharate.Kernel.derivSem]
semantic.eqDecI [in Icharate.Kernel.derivSem]
semantic.eqDecJ [in Icharate.Kernel.derivSem]
semantic.ext [in Icharate.Kernel.derivSem]
semantic.I [in Icharate.Kernel.final_sem]
semantic.I [in Icharate.Kernel.derivSem]
semantic.J [in Icharate.Kernel.final_sem]
semantic.J [in Icharate.Kernel.derivSem]
semantic.lexi [in Icharate.Kernel.final_sem]
semantic.map [in Icharate.Kernel.final_sem]
semantic.map [in Icharate.Kernel.derivSem]
semantic.W [in Icharate.Kernel.final_sem]
semantic.W [in Icharate.Kernel.derivSem]
syntaxNatDed.A [in Icharate.Kernel.natDedGram]
syntaxNatDed.eqdecI [in Icharate.Kernel.natDedGram]
syntaxNatDed.eqdecJ [in Icharate.Kernel.natDedGram]
syntaxNatDed.ext [in Icharate.Kernel.natDedGram]
syntaxNatDed.I [in Icharate.Kernel.natDedGram]
syntaxNatDed.J [in Icharate.Kernel.natDedGram]
syntaxNatDed.lexSyn [in Icharate.Kernel.natDedGram]
syntaxNatDed.W [in Icharate.Kernel.natDedGram]
T
to_coq.W [in Icharate.Kernel.interp_coq]U
unaries.A [in Icharate.Meta.unaries]unaries.decI [in Icharate.Meta.unaries]
unaries.decJ [in Icharate.Meta.unaries]
unaries.I [in Icharate.Meta.unaries]
unaries.J [in Icharate.Meta.unaries]
unaries.W [in Icharate.Meta.unaries]
unboundDepend.A [in Icharate.Meta.unbounDep]
unboundDepend.eqdecI [in Icharate.Meta.unbounDep]
unboundDepend.eqdecJ [in Icharate.Meta.unbounDep]
unboundDepend.ext [in Icharate.Meta.unbounDep]
unboundDepend.I [in Icharate.Meta.unbounDep]
unboundDepend.J [in Icharate.Meta.unbounDep]
unboundDepend.W [in Icharate.Meta.unbounDep]
Library Index
A
apply_rule_propsB
basicsC
crossDepD
dep_exderivedRulesNatDed
derivSem
E
ex1ex1s
ex3
F
final_semI
interp_coqL
lambda_coqlambda_reduction
lambda_bruijn
listAux
logic_const
M
medialExmedialExtraction
N
natDednatDedGram
notations
P
permutationpolarity
polEx
polTac
S
semLexseqNatDed
sequent
struct_tacs
struct_ex
struct_props
T
tacticsDedtacticsSeq
U
unariesunbounDep
Lemma Index
A
access_eq_apply [in Icharate.Kernel.apply_rule_props]access_subCont [in Icharate.Kernel.apply_rule_props]
access_sub_cont [in Icharate.Kernel.apply_rule_props]
access_same_shape [in Icharate.Kernel.apply_rule_props]
access_same_shape_true [in Icharate.Kernel.apply_rule_props]
access_pathR [in Icharate.Kernel.apply_rule_props]
access_pathL [in Icharate.Kernel.apply_rule_props]
access_leaf_false [in Icharate.Kernel.apply_rule_props]
access_is_sub_cont [in Icharate.Kernel.apply_rule_props]
access_leaf [in Icharate.Kernel.apply_rule_props]
access_dec [in Icharate.Kernel.apply_rule_props]
access_some_true [in Icharate.Kernel.apply_rule_props]
access_diam_none [in Icharate.Kernel.apply_rule_props]
access_diam_TDiam [in Icharate.Kernel.apply_rule_props]
access_diam_some [in Icharate.Kernel.apply_rule_props]
access_Com_some [in Icharate.Kernel.apply_rule_props]
access_com_some [in Icharate.Kernel.apply_rule_props]
access_com_none [in Icharate.Kernel.apply_rule_props]
access_res [in Icharate.Kernel.apply_rule_props]
acces_same_shape [in Icharate.Kernel.apply_rule_props]
acces_isLeaf [in Icharate.Kernel.apply_rule_props]
acces_leaf_shape [in Icharate.Kernel.apply_rule_props]
add_in [in Icharate.Lib.permutation]
add_in [in Icharate.Lib.listAux]
allDistinct_to_distinct [in Icharate.Kernel.basics]
apply_rule_same_shape2 [in Icharate.Kernel.apply_rule_props]
apply_rule_same_shape [in Icharate.Kernel.apply_rule_props]
apply_rule_diam [in Icharate.Kernel.apply_rule_props]
apply_rule_com [in Icharate.Kernel.apply_rule_props]
apply_rule_pvar [in Icharate.Kernel.apply_rule_props]
B
Back_antitonicity [in Icharate.Meta.derivedRulesNatDed]betaExtract [in Icharate.Kernel.lambda_reduction]
betaTransitive [in Icharate.Kernel.lambda_reduction]
beta_normal [in Icharate.Kernel.lambda_reduction]
beta_twoL_mono [in Icharate.Kernel.lambda_reduction]
beta_twoL_mono2 [in Icharate.Kernel.lambda_reduction]
beta_twoL_mono1 [in Icharate.Kernel.lambda_reduction]
beta_dediam_mono [in Icharate.Kernel.lambda_reduction]
beta_diam_mono [in Icharate.Kernel.lambda_reduction]
beta_debox_mono [in Icharate.Kernel.lambda_reduction]
beta_pi2_mono [in Icharate.Kernel.lambda_reduction]
beta_pi1_mono [in Icharate.Kernel.lambda_reduction]
beta_box_mono [in Icharate.Kernel.lambda_reduction]
beta_abs_mono [in Icharate.Kernel.lambda_reduction]
beta_app_mono [in Icharate.Kernel.lambda_reduction]
beta_app_mono2 [in Icharate.Kernel.lambda_reduction]
beta_app_mono1 [in Icharate.Kernel.lambda_reduction]
C
comDiamImgInv [in Icharate.Kernel.struct_ex]comDiam_Inv [in Icharate.Kernel.struct_ex]
comDiam_rw [in Icharate.Kernel.struct_ex]
D
deriv1 [in Icharate.Examples.polEx]distinct_add [in Icharate.Lib.listAux]
distinct_app [in Icharate.Lib.listAux]
Dot_monotonicity0 [in Icharate.Meta.derivedRulesNatDed]
Dot_monotonicity [in Icharate.Meta.derivedRulesNatDed]
E
eqdecX_rw [in Icharate.Tacs.struct_tacs]eqDiffDB [in Icharate.Meta.unaries]
eqDiffDiamBox [in Icharate.Meta.unaries]
eqmset_to_ind [in Icharate.Lib.permutation]
extract_forall [in Icharate.Lib.listAux]
extract_permut [in Icharate.Lib.listAux]
extract_app [in Icharate.Lib.listAux]
extract_one [in Icharate.Lib.listAux]
F
forall_eq_list [in Icharate.Lib.listAux]G
getTypeAbs [in Icharate.Kernel.lambda_bruijn]getTypeAppl [in Icharate.Kernel.lambda_bruijn]
getTypeBox [in Icharate.Kernel.lambda_bruijn]
getTypeDebox [in Icharate.Kernel.lambda_bruijn]
getTypeDediam [in Icharate.Kernel.lambda_bruijn]
getTypeDiam [in Icharate.Kernel.lambda_bruijn]
getTypePi1 [in Icharate.Kernel.lambda_bruijn]
getTypePi2 [in Icharate.Kernel.lambda_bruijn]
getTypeTwoL [in Icharate.Kernel.lambda_bruijn]
I
incDiamImgInv [in Icharate.Kernel.struct_ex]incDiam_Inv [in Icharate.Kernel.struct_ex]
incl_distinct_permut [in Icharate.Lib.listAux]
ind_permu_to_eqmset [in Icharate.Lib.permutation]
in_isLeaf [in Icharate.Kernel.basics]
isIncluded_to_isIncl [in Icharate.Kernel.basics]
isIncl_app [in Icharate.Lib.listAux]
isIncl_in [in Icharate.Lib.listAux]
isLeaf_in [in Icharate.Kernel.basics]
isWellFormedBind [in Icharate.Kernel.lambda_bruijn]
isWellFormedBindN [in Icharate.Kernel.lambda_bruijn]
isWellFormedSubst [in Icharate.Kernel.lambda_bruijn]
isWFStrictSub [in Icharate.Kernel.lambda_reduction]
K
KDiamImgInv [in Icharate.Kernel.struct_ex]KDiam_Inv [in Icharate.Kernel.struct_ex]
KDiam_rw [in Icharate.Kernel.struct_ex]
K2DiamImgInv [in Icharate.Kernel.struct_ex]
K2Diam_Inv [in Icharate.Kernel.struct_ex]
K2Diam_rw [in Icharate.Kernel.struct_ex]
K2Diam_ws [in Icharate.Kernel.struct_ex]
L
leftLinear_Diam [in Icharate.Kernel.struct_props]leftLinear_Com2 [in Icharate.Kernel.struct_props]
leftLinear_Com1 [in Icharate.Kernel.struct_props]
length_app [in Icharate.Lib.permutation]
lift_wf [in Icharate.Kernel.lambda_bruijn]
linearPolarity [in Icharate.Meta.polarity]
linearTocondStruct [in Icharate.Meta.unaries]
linear_permut [in Icharate.Kernel.struct_props]
linear_pol [in Icharate.Tacs.polTac]
L1ImgInv [in Icharate.Kernel.struct_ex]
L1_Inv [in Icharate.Kernel.struct_ex]
L1_rw [in Icharate.Kernel.struct_ex]
L2ImgInv [in Icharate.Kernel.struct_ex]
L2_Inv [in Icharate.Kernel.struct_ex]
L2_rw [in Icharate.Kernel.struct_ex]
M
map_permut [in Icharate.Lib.permutation]map_app [in Icharate.Lib.permutation]
map_length [in Icharate.Lib.listAux]
match_strip [in Icharate.Kernel.basics]
MA1ImgInv [in Icharate.Kernel.struct_ex]
MA1_Inv [in Icharate.Kernel.struct_ex]
MA1_rw [in Icharate.Kernel.struct_ex]
MA2DiamImgInv [in Icharate.Kernel.struct_ex]
MA2Diam_Inv [in Icharate.Kernel.struct_ex]
MA2Diam_rw [in Icharate.Kernel.struct_ex]
MA2ImgInv [in Icharate.Kernel.struct_ex]
MA2_Inv [in Icharate.Kernel.struct_ex]
MA2_rw [in Icharate.Kernel.struct_ex]
MCImgInv [in Icharate.Kernel.struct_ex]
MC_Inv [in Icharate.Kernel.struct_ex]
MC_rw [in Icharate.Kernel.struct_ex]
MPDiamImgInv [in Icharate.Kernel.struct_ex]
MPDiam_Inv [in Icharate.Kernel.struct_ex]
MPDiam_rw [in Icharate.Kernel.struct_ex]
MPImgInv [in Icharate.Kernel.struct_ex]
MP_Inv [in Icharate.Kernel.struct_ex]
MP_rw [in Icharate.Kernel.struct_ex]
MP1DiamImgInv [in Icharate.Kernel.struct_ex]
MP1Diam_Inv [in Icharate.Kernel.struct_ex]
MP1Diam_rw [in Icharate.Kernel.struct_ex]
MP2DiamImgInv [in Icharate.Kernel.struct_ex]
MP2Diam_Inv [in Icharate.Kernel.struct_ex]
MP2Diam_rw [in Icharate.Kernel.struct_ex]
multiplicity_one_distinct [in Icharate.Lib.listAux]
multiplicity_0_notIn [in Icharate.Lib.listAux]
mult_add_somewhere2 [in Icharate.Lib.permutation]
mult_add_somewhere1 [in Icharate.Lib.permutation]
mult_In [in Icharate.Lib.permutation]
mult_app [in Icharate.Lib.permutation]
N
noIntersectionLeaf [in Icharate.Kernel.basics]noInter_pattern_to_list [in Icharate.Kernel.basics]
noInter_app [in Icharate.Lib.listAux]
normalFormExtr [in Icharate.Kernel.lambda_reduction]
notWellFormedNum [in Icharate.Kernel.lambda_bruijn]
no_holes [in Icharate.Kernel.basics]
nth_flatten_leaf [in Icharate.Kernel.basics]
nth_add3 [in Icharate.Kernel.lambda_bruijn]
nth_add2 [in Icharate.Kernel.lambda_bruijn]
nth_add1 [in Icharate.Kernel.lambda_bruijn]
nth_error_scd_app [in Icharate.Lib.listAux]
nth_error_fst_app [in Icharate.Lib.listAux]
nth_error_app [in Icharate.Lib.listAux]
nth_error_some_length [in Icharate.Lib.listAux]
nth_error_length [in Icharate.Lib.listAux]
nth_sup_length [in Icharate.Lib.listAux]
nth_map [in Icharate.Lib.listAux]
O
one_type [in Icharate.Kernel.lambda_bruijn]op_all_permut [in Icharate.Lib.permutation]
op_all_app [in Icharate.Lib.permutation]
P
permutation_add' [in Icharate.Lib.permutation]permutation_uncons [in Icharate.Lib.permutation]
permutation_nil [in Icharate.Lib.permutation]
permut_add_a [in Icharate.Lib.permutation]
permut_app_same_l [in Icharate.Lib.permutation]
permut_sym [in Icharate.Lib.permutation]
permut_app_com [in Icharate.Lib.permutation]
permut_nil2 [in Icharate.Lib.permutation]
permut_nil1 [in Icharate.Lib.permutation]
permut_length [in Icharate.Lib.permutation]
permut_sub_cont [in Icharate.Kernel.apply_rule_props]
permut_same_pol [in Icharate.Meta.polarity]
permut_extract [in Icharate.Lib.listAux]
PImgInv [in Icharate.Kernel.struct_ex]
polarityDed [in Icharate.Meta.polarity]
polarityRef [in Icharate.Meta.polarity]
polarityRefDed [in Icharate.Meta.polarity]
polaritySeq [in Icharate.Meta.polarity]
proof_irrelevanceA [in Icharate.Tacs.struct_tacs]
P_Inv [in Icharate.Kernel.struct_ex]
P_rw [in Icharate.Kernel.struct_ex]
R
redexAppl [in Icharate.Kernel.lambda_reduction]redexDebox [in Icharate.Kernel.lambda_reduction]
redexDediam [in Icharate.Kernel.lambda_reduction]
redexNF [in Icharate.Kernel.lambda_reduction]
redexPi1 [in Icharate.Kernel.lambda_reduction]
redexPi2 [in Icharate.Kernel.lambda_reduction]
reduceAllBeta [in Icharate.Kernel.lambda_reduction]
reduceAllWellFound [in Icharate.Kernel.lambda_reduction]
replaceDB [in Icharate.Meta.unaries]
replacePolarity [in Icharate.Meta.polarity]
replaceStruct [in Icharate.Meta.polarity]
S
same_type_after_subst [in Icharate.Kernel.final_sem]same_shape_par_replace [in Icharate.Kernel.basics]
same_shape_SubCont [in Icharate.Kernel.basics]
semWellDefined [in Icharate.Kernel.derivSem]
sem_wt [in Icharate.Kernel.final_sem]
simplBetaToRefTrans [in Icharate.Kernel.lambda_reduction]
strip_match [in Icharate.Kernel.basics]
structRepDB [in Icharate.Meta.unaries]
subCont_length [in Icharate.Kernel.basics]
subCont_same_shape [in Icharate.Kernel.basics]
sub_eq_strict [in Icharate.Kernel.lambda_reduction]
sub_cont_pol [in Icharate.Meta.polarity]
T
type_check_wellTyped [in Icharate.Kernel.lambda_bruijn]W
wellFLe [in Icharate.Kernel.lambda_bruijn]wellFLe1 [in Icharate.Kernel.lambda_bruijn]
wellFLe2 [in Icharate.Kernel.lambda_bruijn]
wellFormedUp [in Icharate.Kernel.lambda_bruijn]
wellFormNSub [in Icharate.Kernel.lambda_bruijn]
wellTypedAbs [in Icharate.Kernel.lambda_bruijn]
wellTypedAppEnv [in Icharate.Kernel.lambda_bruijn]
wellTypedBind [in Icharate.Kernel.lambda_bruijn]
wellTypedFormed [in Icharate.Kernel.lambda_bruijn]
wellTypedSem [in Icharate.Kernel.derivSem]
wellTypedSub [in Icharate.Kernel.lambda_bruijn]
wellTypedSubst [in Icharate.Kernel.lambda_bruijn]
wellTyped_deriv_sem [in Icharate.Kernel.derivSem]
wellTyped_type_check [in Icharate.Kernel.lambda_bruijn]
well_typed_no_empty [in Icharate.Kernel.semLex]
wf_lex [in Icharate.Examples.ex1s]
Z
zfill_fill [in Icharate.Kernel.basics]zfill_fill_0 [in Icharate.Kernel.basics]
zgraft_def [in Icharate.Kernel.basics]
Constructor Index
A
a [in Icharate.Examples.polEx]a [in Icharate.Examples.ex1]
a [in Icharate.Examples.ex1s]
abs [in Icharate.Kernel.lambda_bruijn]
absRed [in Icharate.Kernel.lambda_reduction]
absRed2 [in Icharate.Kernel.lambda_reduction]
add_rule [in Icharate.Kernel.basics]
add_next [in Icharate.Kernel.lambda_bruijn]
add_0 [in Icharate.Kernel.lambda_bruijn]
add_2 [in Icharate.Lib.permutation]
add_fst [in Icharate.Lib.permutation]
AND [in Icharate.Kernel.logic_const]
appl [in Icharate.Kernel.lambda_bruijn]
applRed1 [in Icharate.Kernel.lambda_reduction]
applRed2 [in Icharate.Kernel.lambda_reduction]
At [in Icharate.Kernel.basics]
Ax [in Icharate.Kernel.sequent]
B
BackE [in Icharate.Kernel.natDed]BackI [in Icharate.Kernel.natDed]
Backslash [in Icharate.Kernel.basics]
bComma [in Icharate.Kernel.basics]
bDiamond [in Icharate.Kernel.basics]
betaRefl [in Icharate.Kernel.lambda_reduction]
betaTrans [in Icharate.Kernel.lambda_reduction]
Box [in Icharate.Kernel.basics]
box [in Icharate.Kernel.lambda_bruijn]
boxDeboxRed [in Icharate.Kernel.lambda_reduction]
BoxE [in Icharate.Kernel.natDed]
BoxI [in Icharate.Kernel.natDed]
boxRed [in Icharate.Kernel.lambda_reduction]
C
cartProd [in Icharate.Kernel.lambda_bruijn]Comma [in Icharate.Kernel.basics]
comma_matches [in Icharate.Kernel.basics]
completement [in Icharate.Examples.medialEx]
comW [in Icharate.Tacs.tacticsDed]
com_eqv [in Icharate.Kernel.basics]
consT [in Icharate.Kernel.lambda_coq]
cons_trans [in Icharate.Kernel.lambda_coq]
CutRule [in Icharate.Kernel.sequent]
D
debox [in Icharate.Kernel.lambda_bruijn]deboxRed [in Icharate.Kernel.lambda_reduction]
dediam [in Icharate.Kernel.lambda_bruijn]
dediamRed [in Icharate.Kernel.lambda_reduction]
diam [in Icharate.Kernel.lambda_bruijn]
diamDediamRed [in Icharate.Kernel.lambda_reduction]
DiamE [in Icharate.Kernel.natDed]
DiamI [in Icharate.Kernel.natDed]
Diamond [in Icharate.Kernel.basics]
diamRed [in Icharate.Kernel.lambda_reduction]
diamW [in Icharate.Tacs.tacticsDed]
diam_eqv [in Icharate.Kernel.basics]
diam_matches [in Icharate.Kernel.basics]
Dot [in Icharate.Kernel.basics]
DotE [in Icharate.Kernel.natDed]
DotI [in Icharate.Kernel.natDed]
dP [in Icharate.Tacs.tacticsDed]
E
e [in Icharate.Kernel.lambda_bruijn]EX [in Icharate.Kernel.logic_const]
excons [in Icharate.Lib.listAux]
exnil [in Icharate.Lib.listAux]
EXU [in Icharate.Kernel.logic_const]
F
FORALL [in Icharate.Kernel.logic_const]form [in Icharate.Kernel.basics]
formal [in Icharate.Kernel.final_sem]
form_eqv [in Icharate.Kernel.basics]
form_matches [in Icharate.Kernel.basics]
funAppli [in Icharate.Kernel.lambda_bruijn]
H
hasNF1 [in Icharate.Kernel.lambda_reduction]has_pdiam [in Icharate.Kernel.basics]
has_pcom [in Icharate.Kernel.basics]
has_pvar [in Icharate.Kernel.basics]
hComma [in Icharate.Kernel.basics]
hDiamond [in Icharate.Kernel.basics]
hole [in Icharate.Kernel.basics]
Houda [in Icharate.Examples.polEx]
hres [in Icharate.Kernel.basics]
hyp [in Icharate.Kernel.basics]
hyps [in Icharate.Kernel.lambda_bruijn]
I
ignore [in Icharate.Examples.polEx]ignore [in Icharate.Examples.medialEx]
ignore [in Icharate.Examples.ex1]
ignore [in Icharate.Examples.ex1s]
IMPL [in Icharate.Kernel.logic_const]
intention [in Icharate.Kernel.lambda_bruijn]
in_extension_right [in Icharate.Kernel.basics]
in_extension_rule [in Icharate.Kernel.basics]
L
la [in Icharate.Examples.polEx]la [in Icharate.Examples.ex1]
la [in Icharate.Examples.ex1s]
LBack [in Icharate.Kernel.sequent]
LBox [in Icharate.Kernel.sequent]
LDiam [in Icharate.Kernel.sequent]
LDot [in Icharate.Kernel.sequent]
likes [in Icharate.Examples.dep_ex]
lP [in Icharate.Tacs.tacticsDed]
LSlash [in Icharate.Kernel.sequent]
M
Marie [in Icharate.Examples.medialEx]Mary [in Icharate.Examples.dep_ex]
mk_gramS [in Icharate.Kernel.natDedGram]
mk_lexS [in Icharate.Kernel.natDedGram]
mk_gram [in Icharate.Kernel.semLex]
mk_lex [in Icharate.Kernel.semLex]
m1 [in Icharate.Examples.medialEx]
m1 [in Icharate.Examples.dep_ex]
m2 [in Icharate.Examples.medialEx]
m2 [in Icharate.Examples.dep_ex]
N
n [in Icharate.Examples.polEx]n [in Icharate.Examples.medialEx]
n [in Icharate.Examples.dep_ex]
n [in Icharate.Examples.ex1]
n [in Icharate.Examples.ex1s]
nilT [in Icharate.Kernel.lambda_coq]
nil_trans [in Icharate.Kernel.lambda_coq]
NL [in Icharate.Kernel.basics]
NoneT [in Icharate.Kernel.lambda_coq]
noRep [in Icharate.Meta.derivedRulesNatDed]
normal [in Icharate.Kernel.final_sem]
np [in Icharate.Examples.polEx]
np [in Icharate.Examples.medialEx]
np [in Icharate.Examples.dep_ex]
np [in Icharate.Examples.ex1]
np [in Icharate.Examples.ex1s]
num [in Icharate.Kernel.lambda_bruijn]
O
obj1 [in Icharate.Kernel.lambda_coq]oneW [in Icharate.Tacs.tacticsDed]
OR [in Icharate.Kernel.logic_const]
P
par_replaceDiamond [in Icharate.Kernel.basics]par_replaceBin [in Icharate.Kernel.basics]
par_root [in Icharate.Kernel.basics]
par_zero [in Icharate.Kernel.basics]
pcomma [in Icharate.Kernel.basics]
pdiam [in Icharate.Kernel.basics]
perm_trans [in Icharate.Lib.permutation]
perm_app [in Icharate.Lib.permutation]
perm_cons [in Icharate.Lib.permutation]
perm_refl [in Icharate.Lib.permutation]
Peter [in Icharate.Examples.dep_ex]
piRed1 [in Icharate.Kernel.lambda_reduction]
piRed2 [in Icharate.Kernel.lambda_reduction]
pi1 [in Icharate.Kernel.lambda_bruijn]
pi1Red [in Icharate.Kernel.lambda_reduction]
pi2 [in Icharate.Kernel.lambda_bruijn]
pi2Red [in Icharate.Kernel.lambda_reduction]
pvar [in Icharate.Kernel.basics]
Q
que [in Icharate.Examples.polEx]que [in Icharate.Examples.medialEx]
que [in Icharate.Examples.ex1]
que [in Icharate.Examples.ex1s]
R
raison [in Icharate.Examples.polEx]raison [in Icharate.Examples.ex1]
raison [in Icharate.Examples.ex1s]
RBack [in Icharate.Kernel.sequent]
RBox [in Icharate.Kernel.sequent]
RDiam [in Icharate.Kernel.sequent]
RDot [in Icharate.Kernel.sequent]
reduce1 [in Icharate.Kernel.natDedGram]
replaceDiamond [in Icharate.Kernel.basics]
replaceLeft [in Icharate.Kernel.basics]
replaceRight [in Icharate.Kernel.basics]
replaceRoot [in Icharate.Kernel.basics]
repRu [in Icharate.Meta.derivedRulesNatDed]
rep1 [in Icharate.Meta.derivedRulesNatDed]
rep2 [in Icharate.Meta.derivedRulesNatDed]
res [in Icharate.Kernel.basics]
ress [in Icharate.Kernel.lambda_bruijn]
rP [in Icharate.Tacs.tacticsDed]
RSlash [in Icharate.Kernel.sequent]
rstruct_replaceRight [in Icharate.Kernel.basics]
S
s [in Icharate.Examples.polEx]s [in Icharate.Examples.medialEx]
s [in Icharate.Examples.dep_ex]
s [in Icharate.Examples.ex1]
s [in Icharate.Examples.ex1s]
sameT [in Icharate.Kernel.lambda_reduction]
same_shape_diam [in Icharate.Kernel.basics]
same_shape_comma [in Icharate.Kernel.basics]
same_shape_leaf [in Icharate.Kernel.basics]
Slash [in Icharate.Kernel.basics]
SlashE [in Icharate.Kernel.natDed]
SlashI [in Icharate.Kernel.natDed]
SomeT [in Icharate.Kernel.lambda_coq]
ssubAbs [in Icharate.Kernel.lambda_reduction]
ssubAppl1 [in Icharate.Kernel.lambda_reduction]
ssubAppl2 [in Icharate.Kernel.lambda_reduction]
ssubBox [in Icharate.Kernel.lambda_reduction]
ssubDebox [in Icharate.Kernel.lambda_reduction]
ssubDediam [in Icharate.Kernel.lambda_reduction]
ssubDiam [in Icharate.Kernel.lambda_reduction]
ssubPi1 [in Icharate.Kernel.lambda_reduction]
ssubPi2 [in Icharate.Kernel.lambda_reduction]
ssubTwoL1 [in Icharate.Kernel.lambda_reduction]
ssubTwoL2 [in Icharate.Kernel.lambda_reduction]
StructR [in Icharate.Kernel.sequent]
StructRule [in Icharate.Kernel.natDed]
struct_replaceDiamond [in Icharate.Kernel.basics]
struct_replaceLeft [in Icharate.Kernel.basics]
struct_replaceRoot [in Icharate.Kernel.basics]
subAbs [in Icharate.Kernel.lambda_reduction]
subAppl1 [in Icharate.Kernel.lambda_reduction]
subAppl2 [in Icharate.Kernel.lambda_reduction]
subBox [in Icharate.Kernel.lambda_reduction]
subDebox [in Icharate.Kernel.lambda_reduction]
subDediam [in Icharate.Kernel.lambda_reduction]
subDiam [in Icharate.Kernel.lambda_reduction]
subPi1 [in Icharate.Kernel.lambda_reduction]
subPi2 [in Icharate.Kernel.lambda_reduction]
subTwoL1 [in Icharate.Kernel.lambda_reduction]
subTwoL2 [in Icharate.Kernel.lambda_reduction]
sub_diam [in Icharate.Kernel.basics]
sub_right [in Icharate.Kernel.basics]
sub_left [in Icharate.Kernel.basics]
sub_all [in Icharate.Kernel.basics]
T
t [in Icharate.Kernel.lambda_bruijn]TDiamond [in Icharate.Kernel.basics]
thinks [in Icharate.Examples.dep_ex]
twoL [in Icharate.Kernel.lambda_bruijn]
twoLRed1 [in Icharate.Kernel.lambda_reduction]
twoLRed2 [in Icharate.Kernel.lambda_reduction]
typeAbs [in Icharate.Kernel.lambda_bruijn]
typeAppl [in Icharate.Kernel.lambda_bruijn]
typeBox [in Icharate.Kernel.lambda_bruijn]
typeDebox [in Icharate.Kernel.lambda_bruijn]
typeDediam [in Icharate.Kernel.lambda_bruijn]
typeDiam [in Icharate.Kernel.lambda_bruijn]
typeHyps [in Icharate.Kernel.lambda_bruijn]
typeNum [in Icharate.Kernel.lambda_bruijn]
typePi1 [in Icharate.Kernel.lambda_bruijn]
typePi2 [in Icharate.Kernel.lambda_bruijn]
typeTwoL [in Icharate.Kernel.lambda_bruijn]
typeVar [in Icharate.Kernel.lambda_bruijn]
W
Wd [in Icharate.Kernel.natDed]whom [in Icharate.Examples.dep_ex]
word [in Icharate.Kernel.basics]
wt [in Icharate.Kernel.derivSem]
Z
zdown [in Icharate.Kernel.basics]zleft [in Icharate.Kernel.basics]
zright [in Icharate.Kernel.basics]
zroot [in Icharate.Kernel.basics]
Axiom Index
B
bapply_rule [in Icharate.Kernel.basics]box_coq [in Icharate.Kernel.lambda_coq]
D
debox_coq [in Icharate.Kernel.lambda_coq]dediam_coq [in Icharate.Kernel.lambda_coq]
diam_coq [in Icharate.Kernel.lambda_coq]
E
E [in Icharate.Kernel.lambda_coq]I
intent [in Icharate.Kernel.lambda_coq]S
semW [in Icharate.Kernel.interp_coq]Inductive Index
A
A [in Icharate.Examples.polEx]A [in Icharate.Examples.medialEx]
A [in Icharate.Examples.dep_ex]
A [in Icharate.Examples.ex1]
A [in Icharate.Examples.ex1s]
add_ith_list [in Icharate.Kernel.lambda_bruijn]
add_somewhere [in Icharate.Lib.permutation]
B
bcontext [in Icharate.Kernel.basics]beta_reduction [in Icharate.Kernel.lambda_reduction]
beta_one_step [in Icharate.Kernel.lambda_reduction]
C
context [in Icharate.Kernel.basics]contextW [in Icharate.Tacs.tacticsDed]
context_eqv [in Icharate.Kernel.basics]
cst [in Icharate.Kernel.final_sem]
E
extension [in Icharate.Kernel.basics]extract_opt [in Icharate.Lib.listAux]
F
Form [in Icharate.Kernel.basics]G
gentzen [in Icharate.Kernel.sequent]H
hasNormalForm [in Icharate.Kernel.lambda_reduction]hasSubContexts [in Icharate.Kernel.basics]
hcontext [in Icharate.Kernel.basics]
I
I [in Icharate.Examples.polEx]I [in Icharate.Examples.medialEx]
I [in Icharate.Examples.dep_ex]
I [in Icharate.Examples.ex1]
I [in Icharate.Examples.ex1s]
in_extension [in Icharate.Kernel.basics]
isStrictSubTerm [in Icharate.Kernel.lambda_reduction]
isSubTerm [in Icharate.Kernel.lambda_reduction]
isWellTyped [in Icharate.Kernel.lambda_bruijn]
is_sub_cont [in Icharate.Kernel.basics]
J
J [in Icharate.Examples.polEx]J [in Icharate.Examples.medialEx]
J [in Icharate.Examples.dep_ex]
J [in Icharate.Examples.ex1]
J [in Icharate.Examples.ex1s]
L
lambda_terms [in Icharate.Kernel.lambda_bruijn]listT [in Icharate.Kernel.lambda_coq]
logic_cst [in Icharate.Kernel.logic_const]
M
matches [in Icharate.Kernel.basics]N
natded [in Icharate.Kernel.natDed]O
optionT [in Icharate.Kernel.lambda_coq]P
par_replace [in Icharate.Kernel.basics]path [in Icharate.Tacs.tacticsDed]
permut [in Icharate.Lib.permutation]
R
reduceTo [in Icharate.Kernel.natDedGram]replace [in Icharate.Kernel.basics]
replaceNTimes [in Icharate.Meta.derivedRulesNatDed]
replaceNTimesExt [in Icharate.Meta.derivedRulesNatDed]
resource [in Icharate.Kernel.basics]
rule_pattern [in Icharate.Kernel.basics]
S
same_shape [in Icharate.Kernel.basics]semType [in Icharate.Kernel.lambda_bruijn]
struct_replace [in Icharate.Kernel.basics]
T
trans_env [in Icharate.Kernel.lambda_coq]type_obj [in Icharate.Kernel.lambda_coq]
W
W [in Icharate.Examples.polEx]W [in Icharate.Examples.medialEx]
W [in Icharate.Examples.dep_ex]
W [in Icharate.Examples.ex1]
W [in Icharate.Examples.ex1s]
word_type [in Icharate.Kernel.derivSem]
Z
zcontext [in Icharate.Kernel.basics]Projection Index
A
A [in Icharate.Kernel.semLex]A_syn [in Icharate.Kernel.natDedGram]
E
eqdecA [in Icharate.Kernel.semLex]eqdecA_syn [in Icharate.Kernel.natDedGram]
eqdecI [in Icharate.Kernel.semLex]
eqdecI_syn [in Icharate.Kernel.natDedGram]
eqdecJ [in Icharate.Kernel.semLex]
eqdecJ_syn [in Icharate.Kernel.natDedGram]
ext [in Icharate.Kernel.semLex]
ext_syn [in Icharate.Kernel.natDedGram]
I
I [in Icharate.Kernel.semLex]I_syn [in Icharate.Kernel.natDedGram]
J
J [in Icharate.Kernel.semLex]J_syn [in Icharate.Kernel.natDedGram]
L
lex [in Icharate.Kernel.semLex]lexic [in Icharate.Kernel.semLex]
lexic_syn [in Icharate.Kernel.natDedGram]
lex_syn [in Icharate.Kernel.natDedGram]
M
map [in Icharate.Kernel.semLex]W
W [in Icharate.Kernel.semLex]wt_lex [in Icharate.Kernel.semLex]
W_syn [in Icharate.Kernel.natDedGram]
Section Index
A
allSem [in Icharate.Kernel.lambda_bruijn]allSem.lambdaX [in Icharate.Kernel.lambda_bruijn]
B
beta [in Icharate.Kernel.lambda_reduction]C
classes [in Icharate.Kernel.struct_props]coq_terms [in Icharate.Kernel.lambda_coq]
cross_dep [in Icharate.Meta.crossDep]
D
Definitions [in Icharate.Kernel.basics]Definitions.Main [in Icharate.Kernel.basics]
Definitions.Main.formulae_etc [in Icharate.Kernel.basics]
Definitions.Main.rep [in Icharate.Kernel.basics]
Definitions.Main.rep.struct_replace_def [in Icharate.Kernel.basics]
defs [in Icharate.Kernel.sequent]
L
lambda_morphism [in Icharate.Kernel.final_sem]M
Main [in Icharate.Kernel.natDed]medialMeta [in Icharate.Meta.medialExtraction]
N
natDedSeq [in Icharate.Meta.seqNatDed]P
perm [in Icharate.Lib.permutation]permt [in Icharate.Lib.listAux]
perm.op_permut [in Icharate.Lib.permutation]
pol [in Icharate.Meta.polarity]
props [in Icharate.Meta.derivedRulesNatDed]
props [in Icharate.Kernel.apply_rule_props]
props.L [in Icharate.Meta.derivedRulesNatDed]
props.LP [in Icharate.Meta.derivedRulesNatDed]
props.MC [in Icharate.Meta.derivedRulesNatDed]
props.MP [in Icharate.Meta.derivedRulesNatDed]
props.P [in Icharate.Meta.derivedRulesNatDed]
R
replace_props [in Icharate.Kernel.basics]S
semantic [in Icharate.Kernel.final_sem]semantic [in Icharate.Kernel.derivSem]
syntaxNatDed [in Icharate.Kernel.natDedGram]
T
to_coq [in Icharate.Kernel.interp_coq]U
unaries [in Icharate.Meta.unaries]unboundDepend [in Icharate.Meta.unbounDep]
Definition Index
A
access [in Icharate.Kernel.basics]access_par_replace [in Icharate.Kernel.apply_rule_props]
access_tac [in Icharate.Tacs.tacticsDed]
addToEnd [in Icharate.Meta.unbounDep]
add_extension [in Icharate.Kernel.basics]
allDistinctLeaves [in Icharate.Kernel.basics]
application_r [in Icharate.Meta.derivedRulesNatDed]
application_l [in Icharate.Meta.derivedRulesNatDed]
apply_rule [in Icharate.Kernel.basics]
apply_rule_par_replace [in Icharate.Kernel.apply_rule_props]
apply_rule_tac [in Icharate.Tacs.tacticsDed]
argument_lowering [in Icharate.Meta.derivedRulesNatDed]
axiomGen [in Icharate.Meta.derivedRulesNatDed]
B
Back_lifting [in Icharate.Meta.derivedRulesNatDed]boxDiam [in Icharate.Meta.derivedRulesNatDed]
box2diam [in Icharate.Meta.derivedRulesNatDed]
C
clause [in Icharate.Examples.ex1]clause [in Icharate.Examples.ex1s]
clause_tree [in Icharate.Examples.ex1]
comDiam [in Icharate.Kernel.struct_ex]
compile [in Icharate.Kernel.basics]
compile_tac [in Icharate.Tacs.tacticsDed]
composition_Back [in Icharate.Meta.derivedRulesNatDed]
composition_Slash [in Icharate.Meta.derivedRulesNatDed]
condExt [in Icharate.Meta.unaries]
condStruct [in Icharate.Meta.unaries]
constructList [in Icharate.Tacs.tacticsDed]
constructList [in Icharate.Lib.listAux]
cont [in Icharate.Examples.polEx]
containsNoRedex [in Icharate.Kernel.lambda_reduction]
contextToForm [in Icharate.Kernel.basics]
context_equiv [in Icharate.Kernel.basics]
context_strip [in Icharate.Kernel.basics]
context_inject [in Icharate.Kernel.basics]
countDiam [in Icharate.Kernel.struct_props]
co_application_r [in Icharate.Meta.derivedRulesNatDed]
co_application_l [in Icharate.Meta.derivedRulesNatDed]
cross_depend [in Icharate.Meta.crossDep]
currying_Back [in Icharate.Meta.derivedRulesNatDed]
currying_Slash [in Icharate.Meta.derivedRulesNatDed]
cut_rule' [in Icharate.Meta.derivedRulesNatDed]
cut_rule1 [in Icharate.Meta.derivedRulesNatDed]
cut_rule [in Icharate.Meta.derivedRulesNatDed]
D
deep_to_shallow [in Icharate.Kernel.interp_coq]deriveTo [in Icharate.Kernel.semLex]
deriveToSyn [in Icharate.Kernel.natDedGram]
deriv1 [in Icharate.Examples.ex1]
deriv1 [in Icharate.Examples.ex1s]
deriv2 [in Icharate.Examples.ex1]
De_currying_Back [in Icharate.Meta.derivedRulesNatDed]
De_currying_Slash [in Icharate.Meta.derivedRulesNatDed]
diamBox [in Icharate.Meta.derivedRulesNatDed]
DiamondE' [in Icharate.Kernel.natDed]
diam_Box [in Icharate.Meta.derivedRulesNatDed]
diffDBTerm [in Icharate.Meta.unaries]
diffDiamBox [in Icharate.Meta.unaries]
distDiam [in Icharate.Meta.crossDep]
distinct_elts [in Icharate.Lib.listAux]
DotE' [in Icharate.Kernel.natDed]
doubleReplacePar [in Icharate.Kernel.basics]
E
eqdec [in Icharate.Kernel.basics]eqdecA [in Icharate.Examples.polEx]
eqdecA [in Icharate.Examples.medialEx]
eqdecA [in Icharate.Examples.dep_ex]
eqdecA [in Icharate.Examples.ex1]
eqdecA [in Icharate.Examples.ex1s]
eqdecC [in Icharate.Kernel.basics]
eqDecF [in Icharate.Kernel.basics]
eqdecI [in Icharate.Examples.polEx]
eqdecI [in Icharate.Examples.medialEx]
eqdecI [in Icharate.Examples.dep_ex]
eqdecI [in Icharate.Examples.ex1]
eqdecI [in Icharate.Examples.ex1s]
eqdecJ [in Icharate.Examples.polEx]
eqdecJ [in Icharate.Examples.medialEx]
eqdecJ [in Icharate.Examples.dep_ex]
eqdecJ [in Icharate.Examples.ex1]
eqdecJ [in Icharate.Examples.ex1s]
eqdecRess [in Icharate.Kernel.basics]
eqDecSem [in Icharate.Kernel.lambda_bruijn]
exchange_r [in Icharate.Meta.derivedRulesNatDed]
exchange_l [in Icharate.Meta.derivedRulesNatDed]
ext [in Icharate.Examples.ex1s]
extractNF [in Icharate.Kernel.lambda_reduction]
extract_lex_syn [in Icharate.Kernel.semLex]
extract_sub_list [in Icharate.Kernel.semLex]
ext1 [in Icharate.Examples.polEx]
ext1 [in Icharate.Examples.medialEx]
ext1 [in Icharate.Examples.dep_ex]
ext1 [in Icharate.Examples.ex1]
F
fill [in Icharate.Kernel.basics]fill_to_par_replace [in Icharate.Kernel.basics]
fitsContSent [in Icharate.Kernel.natDedGram]
fits_aux [in Icharate.Kernel.natDedGram]
flattenCont [in Icharate.Kernel.natDedGram]
flatten_pattern [in Icharate.Kernel.basics]
frag [in Icharate.Examples.medialEx]
free_lambda [in Icharate.Kernel.derivSem]
G
Geach_secondary_Back [in Icharate.Meta.derivedRulesNatDed]Geach_secondary_Slash [in Icharate.Meta.derivedRulesNatDed]
Geach_main_Back [in Icharate.Meta.derivedRulesNatDed]
Geach_main_Slash [in Icharate.Meta.derivedRulesNatDed]
Geach_main_Back [in Icharate.Examples.ex3]
getContext [in Icharate.Tacs.tacticsDed]
getContext1 [in Icharate.Tacs.tacticsDed]
getFirstPathDiam [in Icharate.Tacs.tacticsDed]
getHypForm [in Icharate.Tacs.tacticsDed]
getIthRule [in Icharate.Tacs.tacticsDed]
getSemantic [in Icharate.Kernel.derivSem]
getSubLists [in Icharate.Lib.listAux]
getTermByPath [in Icharate.Tacs.tacticsDed]
getTypeWT [in Icharate.Kernel.derivSem]
gram1 [in Icharate.Examples.polEx]
gram1 [in Icharate.Examples.medialEx]
gram1 [in Icharate.Examples.dep_ex]
gram1 [in Icharate.Examples.ex1]
gram2 [in Icharate.Examples.ex1s]
I
incDiam [in Icharate.Kernel.struct_ex]incDiam_rw [in Icharate.Kernel.struct_ex]
isIncl [in Icharate.Lib.listAux]
isIncluded [in Icharate.Kernel.basics]
isLeaf [in Icharate.Kernel.basics]
isLeaf_dec_com [in Icharate.Kernel.basics]
isLeaf_dec [in Icharate.Kernel.basics]
isWellFormed [in Icharate.Kernel.lambda_bruijn]
isWellFormedN [in Icharate.Kernel.lambda_bruijn]
isWellTyped_lex [in Icharate.Kernel.semLex]
isWellTyped_pairs [in Icharate.Kernel.semLex]
K
KDiam [in Icharate.Kernel.struct_ex]K2Diam [in Icharate.Kernel.struct_ex]
L
lambdaAbs [in Icharate.Kernel.lambda_bruijn]lambdaBind [in Icharate.Kernel.lambda_bruijn]
lambdaSubN [in Icharate.Kernel.lambda_bruijn]
lambSub [in Icharate.Kernel.lambda_bruijn]
leftLinear [in Icharate.Kernel.struct_props]
leftLinearSahlqvist [in Icharate.Kernel.struct_props]
leftLinear_par_replace [in Icharate.Kernel.struct_props]
lengthW [in Icharate.Tacs.tacticsDed]
lex [in Icharate.Examples.polEx]
lex [in Icharate.Examples.medialEx]
lex [in Icharate.Examples.dep_ex]
lex [in Icharate.Examples.ex1]
lex [in Icharate.Examples.ex1s]
lex_opaq [in Icharate.Examples.ex1]
lex1 [in Icharate.Examples.polEx]
lex1 [in Icharate.Examples.medialEx]
lex1 [in Icharate.Examples.dep_ex]
lex1 [in Icharate.Examples.ex1]
lex1' [in Icharate.Examples.polEx]
lex1' [in Icharate.Examples.ex1]
lex2 [in Icharate.Examples.ex1s]
lift_lambda [in Icharate.Kernel.lambda_bruijn]
linear [in Icharate.Kernel.struct_props]
linearDiam [in Icharate.Kernel.struct_props]
linear_ext [in Icharate.Tacs.polTac]
L1 [in Icharate.Kernel.struct_ex]
L2 [in Icharate.Kernel.struct_ex]
M
map [in Icharate.Examples.ex1s]mapExt [in Icharate.Kernel.lambda_bruijn]
matches_inv_Diam [in Icharate.Kernel.basics]
matches_inv_Comma [in Icharate.Kernel.basics]
matches_inv_form [in Icharate.Kernel.basics]
MA1 [in Icharate.Kernel.struct_ex]
MA2 [in Icharate.Kernel.struct_ex]
MA2Diam [in Icharate.Kernel.struct_ex]
MA2DiamRep [in Icharate.Meta.unbounDep]
MC [in Icharate.Kernel.struct_ex]
medialExtraction [in Icharate.Meta.medialExtraction]
mixed_composition_Geach [in Icharate.Meta.derivedRulesNatDed]
mixed_composition_Slash [in Icharate.Meta.derivedRulesNatDed]
mixed_composition_Back [in Icharate.Meta.derivedRulesNatDed]
MonoLeftNRu [in Icharate.Meta.derivedRulesNatDed]
MonoRightNRu [in Icharate.Meta.derivedRulesNatDed]
MP [in Icharate.Kernel.struct_ex]
MPDiam [in Icharate.Kernel.struct_ex]
MP1Diam [in Icharate.Kernel.struct_ex]
MP2Diam [in Icharate.Kernel.struct_ex]
my_contW [in Icharate.Examples.medialEx]
my_contextW [in Icharate.Examples.dep_ex]
my_fragment [in Icharate.Examples.dep_ex]
N
natdedNRep [in Icharate.Meta.derivedRulesNatDed]natDedToSeq [in Icharate.Meta.seqNatDed]
natded_trans [in Icharate.Meta.derivedRulesNatDed]
natded0 [in Icharate.Kernel.natDed]
nf_deriv1 [in Icharate.Examples.ex1s]
noHyps [in Icharate.Examples.ex1s]
noInter [in Icharate.Lib.listAux]
noIntersection [in Icharate.Kernel.basics]
normalForm [in Icharate.Kernel.lambda_reduction]
notLeaf [in Icharate.Kernel.struct_props]
no_hyps_inside [in Icharate.Kernel.lambda_bruijn]
nth_error_T [in Icharate.Kernel.lambda_coq]
O
objectLift [in Icharate.Meta.derivedRulesNatDed]op_all [in Icharate.Lib.permutation]
P
P [in Icharate.Kernel.struct_ex]par_replace_to_fill [in Icharate.Kernel.basics]
Permutation [in Icharate.Meta.derivedRulesNatDed]
Permutation2 [in Icharate.Meta.derivedRulesNatDed]
polF [in Icharate.Meta.polarity]
polT [in Icharate.Meta.polarity]
postponing [in Icharate.Meta.derivedRulesNatDed]
preposing [in Icharate.Meta.derivedRulesNatDed]
pretty_printer0 [in Icharate.Kernel.lambda_coq]
pretty_printer [in Icharate.Kernel.interp_coq]
R
reduceAll [in Icharate.Kernel.lambda_reduction]repDistribute [in Icharate.Meta.crossDep]
repExtnatDed [in Icharate.Meta.derivedRulesNatDed]
replaceExtMonoLeft [in Icharate.Meta.derivedRulesNatDed]
replaceExtMonoRight [in Icharate.Meta.derivedRulesNatDed]
replaceNatDed [in Icharate.Meta.seqNatDed]
replaceParCom [in Icharate.Kernel.basics]
replaceParDiam [in Icharate.Kernel.basics]
replaceProp [in Icharate.Kernel.basics]
replaceTermByTerm [in Icharate.Tacs.tacticsDed]
replace_to_par [in Icharate.Kernel.basics]
replace_to_zfill [in Icharate.Kernel.basics]
replExtMono [in Icharate.Meta.derivedRulesNatDed]
replExtTrans [in Icharate.Meta.derivedRulesNatDed]
replNPermut [in Icharate.Meta.derivedRulesNatDed]
repToParRep [in Icharate.Kernel.basics]
repTransform [in Icharate.Meta.crossDep]
restructuring_r [in Icharate.Meta.derivedRulesNatDed]
restructuring_l [in Icharate.Meta.derivedRulesNatDed]
rightLinear [in Icharate.Kernel.struct_props]
S
sameShapeCom [in Icharate.Kernel.basics]sameShapeDiam [in Icharate.Kernel.basics]
same_type [in Icharate.Kernel.final_sem]
same_shape_left_linear [in Icharate.Kernel.struct_props]
semanticTerm [in Icharate.Kernel.derivSem]
seqToNatded [in Icharate.Meta.seqNatDed]
setSynLex [in Icharate.Kernel.natDedGram]
setTypeLog [in Icharate.Kernel.logic_const]
set_syn_sem_Lex [in Icharate.Kernel.semLex]
simple_cut_rule [in Icharate.Meta.derivedRulesNatDed]
Slash_antitonicity [in Icharate.Meta.derivedRulesNatDed]
Slash_lifting [in Icharate.Meta.derivedRulesNatDed]
structPol [in Icharate.Meta.polarity]
structrule [in Icharate.Kernel.basics]
structrule_subst_commute [in Icharate.Kernel.basics]
Structrule' [in Icharate.Kernel.natDed]
struct_replace_to_zfill [in Icharate.Kernel.basics]
struct_replace_as_zfill [in Icharate.Kernel.basics]
substLamb [in Icharate.Kernel.lambda_reduction]
substVar [in Icharate.Kernel.lambda_reduction]
sum_diff_leaves [in Icharate.Meta.unaries]
sum_all [in Icharate.Lib.listAux]
S_combinator [in Icharate.Meta.derivedRulesNatDed]
T
trans [in Icharate.Kernel.final_sem]transformCont [in Icharate.Meta.crossDep]
translate [in Icharate.Kernel.final_sem]
trans_lamb0 [in Icharate.Kernel.lambda_coq]
trans_lamb [in Icharate.Kernel.lambda_coq]
trans_env_nth [in Icharate.Kernel.lambda_coq]
trans_type [in Icharate.Kernel.lambda_coq]
treeDeri [in Icharate.Examples.medialEx]
treeDeriv [in Icharate.Examples.dep_ex]
type_cst [in Icharate.Kernel.final_sem]
type_check [in Icharate.Kernel.lambda_bruijn]
U
unboundDep [in Icharate.Meta.unbounDep]unboundDepend [in Icharate.Meta.unbounDep]
up_lambda [in Icharate.Kernel.lambda_bruijn]
W
weakSahlqvist [in Icharate.Kernel.struct_props]weak_sahlqvist_ext [in Icharate.Kernel.basics]
weak_sahlqvist_rule [in Icharate.Kernel.basics]
whole_sem [in Icharate.Kernel.final_sem]
word_to_lambda [in Icharate.Kernel.final_sem]
wt [in Icharate.Examples.ex1s]
X
XStructRule [in Icharate.Kernel.natDed]XStructrule' [in Icharate.Kernel.natDed]
Z
zcontext_inject [in Icharate.Kernel.basics]zcontext_inject_aux [in Icharate.Kernel.basics]
zfill [in Icharate.Kernel.basics]
zfill_to_struct_replace_0 [in Icharate.Kernel.basics]
zfill_to_replace [in Icharate.Kernel.basics]
zfill_to_replace_0 [in Icharate.Kernel.basics]
zgraft [in Icharate.Kernel.basics]
Record Index
L
lexicon [in Icharate.Kernel.semLex]S
synGram [in Icharate.Kernel.natDedGram]synLexicon [in Icharate.Kernel.natDedGram]
syn_sem_gram [in Icharate.Kernel.semLex]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1113 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (62 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (145 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (226 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (238 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (63 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (276 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |