Def | | l_disjoint(T;l1;l2) | [l_disjoint] | mb list 2 |
Def | | outl(x) | [outl] | union |
Def | | outr(x) | [outr] | union |
Def | | list_accum(x,a.f(x;a);y;l) | [list_accum] | mb list 1 |
Def | | f[n:=x] | [fappend] | mb nat |
Def | |  x,y,z. t(x;y;z) | [so_lambda3] | mb basic |
Def | | ... | [hide] | mb basic |
Def | | ptn_int(x) | [ptn_int] | mb basic |
Def | | ptn_var(x) | [ptn_var] | mb basic |
Def | | lbl_pr( < x, y > ) | [lbl_pair] | mb basic |
Def | | const_ptn(l) | [const_ptn] | mb basic |
Def | | int_ptn(l) | [int_ptn] | mb basic |
Def | | var_ptn(l) | [var_ptn] | mb basic |
Def | | left_ptn(l) | [left_ptn] | mb basic |
Def | | right_ptn(l) | [right_ptn] | mb basic |
Def | | ground_ptn(p) | [ground_ptn] | mb basic |
Def | | $x | [clbl] | mb basic |
Def | | StAntiSym(T;x,y.R(x;y)) | [st_anti_sym] | rel 1 |
Def | | Irrefl(T;x,y.E(x;y)) | [irrefl] | rel 1 |
Def | | For{T,op,id} x as. f(x) | [for] | list 1 |
Def | | ForHdTl{A,f,k} h::t as. g(h;t) | [for_hdtl] | list 1 |
Def | | mapc(f) | [mapc] | list 1 |
Def | | t_iterate(l;n;t) | [t_iterate] | mb tree |
Def | | left_child(t) | [left_child] | mb tree |
Def | | right_child(t) | [right_child] | mb tree |
Def | | leaf_value(t) | [leaf_value] | mb tree |
Def | | tree_node( < x, y > ) | [node] | mb tree |
Def | | Default = > body
EndSwitch | [switch_default] | prog 1 |
Def | | < x,y > = >
body(x;y) | [case_pair] | prog 1 |
Def | | x::y = >
body(x;y)
cont | [case_cons] | prog 1 |
Def | | [] = >
body
cont | [case_nil] | prog 1 |
Def | | = >
body | [case_it] | prog 1 |
Def | | x:body | [case_bind] | prog 1 |
Def | | < < "a", b > , c, 1 > = >
body(b;c)
cont | [case_pattern1] | prog 1 |
Def | | < a, inl < < "a", b > , c, 1 > > = >
body(a;b;c)
cont | [case_pattern2] | prog 1 |
Def | | < a, inl < < "a", b > , c, 1 > > | [pattern2] | prog 1 |
Def | | union1() | [union1] | prog 1 |
Def | | union1_term1(x) = >
body(x)
cont | [case_union1_term1] | prog 1 |
Def | | union1_term1(x) | [union1_term1] | prog 1 |
Def | | union1_term2(x) = >
body(x)
cont | [case_union1_term2] | prog 1 |
Def | | union1_term2(x) | [union1_term2] | prog 1 |
Def | | union1_term3(x) = >
body(x)
cont | [case_union1_term3] | prog 1 |
Def | | union1_term3(x) | [union1_term3] | prog 1 |
Def | | enum1_switch(value;el1;el2;el3) | [enum1_switch] | prog 1 |
Def | | enum1_el1 = >
body
cont | [case_enum1_el1] | prog 1 |
Def | | enum1_el2 = >
body
cont | [case_enum1_el2] | prog 1 |
Def | | enum1_el3 = >
body
cont | [case_enum1_el3] | prog 1 |
Def | | module1_type(prop) | [module1_type] | prog 1 |
Def | | t.tag | [module1_tag] | prog 1 |
Def | | t.data | [module1_data] | prog 1 |
Def | | module1(tag, data) = >
body(tag;data) | [case_module1] | prog 1 |
Def | | module1(tag, data) | [module1] | prog 1 |
Def | | p q | [bxor] | bool 1 |
Def | | p  q | [rev_bimplies] | bool 1 |
Def | | i j k | [lele] | int 1 |
Def | | S T | [suptype] | int 1 |
Def | | t ...$L | [label] | core |
Def | | ??? | [error] | core |
Def | | I | [icomb] | core |
Def | | K | [kcomb] | core |
Def | | S | [scomb] | core |
Def | | let x,y,z = a in t(x;y;z) | [spread3] | core |
Def | | let w,x,y,z = a in t(w;x;y;z) | [spread4] | core |
Def | | let a,b,c,d,e = u in v(a;b;c;d;e) | [spread5] | core |
Def | | let a,b,c,d,e,f = u in v(a;b;c;d;e;f) | [spread6] | core |
Def | | let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g) | [spread7] | core |
Def | | XM | [xmiddle] | core |
Def | | let x = a in b(x) | [let] | core |
Def | | [x]{T} | [type_inj] | core |
Def | | (first x as s.t. P(x) else d) | [find] | mb list 1 |
Def | | ( x L.P(x)) | [l_all] | mb list 2 |
Def | | agree_on_common(T;as;bs) | [agree_on_common] | mb list 1 |
Def | | interleaving(T;L1;L2;L) | [interleaving] | mb list 2 |
Def | | null(as) | [null] | list 1 |
Def | | last(L) | [last] | mb list 1 |
Def | | compose_flips(L) | [compose_flips] | mb list 2 |
Def | | x before y l | [l_before] | mb list 1 |
Def | | guarded_permutation(T;P) | [guarded_permutation] | mb list 2 |
Def | | swap adjacent[P(x;y)] | [swap_adjacent] | mb list 2 |
Def | | Bij(A; B; f) | [biject] | fun 1 |
Def | | count(x < y in L | P(x;y)) | [count_pairs] | mb list 1 |
Def | | no_repeats(T;l) | [no_repeats] | mb list 2 |
Def | | ( x L.P(x)) | [l_exists] | mb list 2 |
Def | | mapfilter(f;P;L) | [mapfilter] | mb list 2 |
Def | |   | [nat_plus] | int 1 |
Def | | i = j | [pm_equal] | int 2 |
Def | | |i| | [absval] | int 2 |
Def | | Preorder(T;x,y.R(x;y)) | [preorder] | rel 1 |
Def | | EquivRel x,y:T. E(x;y) | [equiv_rel] | rel 1 |
Def | | gcd(a;b) | [gcd] | num thy 1 |
Def | |  x:A. B(x) | [sq_exists] | core |
Def | | CoPrime(a,b) | [coprime] | num thy 1 |
Def | | SqStable(P) | [sq_stable] | core |
Def | | atomic(a) | [atomic] | num thy 1 |
Def | | prime(a) | [prime] | num thy 1 |
Def | | a = b mod m | [eqmod] | num thy 1 |
Def | | fib(n) | [fib] | num thy 1 |
Def | | isl(x) | [isl] | union |
Def | | {i...j} | [int_iseg] | int 1 |
Def | | i j | [ge] | core |
Def | | A List | [listp] | mb list 1 |
Def | | l1 l2 | [iseg] | mb list 1 |
Def | | zip(as;bs) | [zip] | mb list 1 |
Def | | unzip(as) | [unzip] | mb list 1 |
Def | | sublist_occurence(T;L1;L2;f) | [sublist_occurence] | mb list 1 |
Def | | interleaving_occurence(T;L1;L2;L;f1;f2) | [interleaving_occurence] | mb list 1 |
Def | | nondecreasing(f;k) | [nondecreasing] | mb nat |
Def | | fadd(f;g) | [fadd] | mb nat |
Def | | R1 = > R2 | [rel_implies] | mb nat |
Def | | R preserves P | [preserved_by] | mb nat |
Def | | R^-1 | [rel_inverse] | mb nat |
Def | | R1 R2 | [rel_or] | mb nat |
Def | | f^n | [fun_exp] | mb nat |
Def | | search(k;P) | [search] | mb nat |
Def | | P Q | [prop_and] | mb nat |
Def | | (ternary) R preserves P | [preserved_by2] | mb nat |
Def | | dec2bool(d) | [dec2bool] | mb basic |
Def | | Decision | [decision] | mb basic |
Def | | Pattern | [ptn] | mb basic |
Def | | SQType(T) | [sq_type] | sqequal 1 |
Def | | l1 = l2 | [eq_lbl] | mb basic |
Def | | Symmetrize(x,y.R(x;y);a;b) | [symmetrize] | rel 1 |
Def | | IsEqFun(T;eq) | [eqfun_p] | rel 1 |
Def | | strict_part(x,y.R(x;y);a;b) | [strict_part] | rel 1 |
Def | | Linorder(T;x,y.R(x;y)) | [linorder] | rel 1 |
Def | | rev(as) | [reverse] | list 1 |
Def | | as[m..n ] | [segment] | list 1 |
Def | | as\[i] | [reject] | list 1 |
Def | | f{m..n } | [listify] | list 1 |
Def | | A List(n) | [list_n] | list 1 |
Def | | i > j | [gt] | core |
Def | | {...i} | [int_lower] | int 1 |
Def | | imin(a;b) | [imin] | int 2 |
Def | | a -- b | [ndiff] | int 2 |
Def | | Rem(a;n;r) | [rem_nrel] | int 2 |
Def | | a mod n | [modulus] | int 2 |
Def | | a  n | [div_floor] | int 2 |
Def | | WellFnd{i}(A;x,y.R(x;y)) | [wellfounded] | well fnd |
Def | | {i...} | [int_upper] | int 1 |
Def | | A ~~ B | [one_one_corr] | fun 1 |
Def | | Tree(E) | [tree] | mb tree |
Def | | tree_leaf(x) | [tree_leaf] | mb tree |
Def | | is_leaf(t) | [is_leaf] | mb tree |
Def | | enum1() | [enum1] | prog 1 |
Def | | b2i(b) | [b2i] | bool 1 |
Def | | p= q | [eq_bool] | bool 1 |
Def | | Stable{P} | [stable] | core |
Def | | {a:T} | [singleton] | core |
Def | | {!x:T | P(x)} | [unique_set] | core |
Def | | a = !x:T. Q(x) | [uni_sat] | core |
Def | | (x l) | [l_member] | mb list 1 |
Def | | P  Q | [implies] | core |
Def | | x:A. B(x) | [all] | core |
Def | | P & Q | [and] | core |
Def | | x:A. B(x) | [exists] | core |
Def | | disjoint_sublists(T;L1;L2;L) | [disjoint_sublists] | mb list 1 |
Def | | swap(L;i;j) | [swap] | mb list 2 |
Def | | (L o f) | [permute_list] | mb list 2 |
Def | | L1 L2 | [sublist] | mb list 1 |
Def | | ||as|| | [length] | list 1 |
Def | | R^* | [rel_star] | mb nat |
Def | |  | [nat] | int 1 |
Def | | l[i] | [select] | list 1 |
Def | | mklist(n;f) | [mklist] | mb list 1 |
Def | | (i, j) | [flip] | mb nat |
Def | | map(f;as) | [map] | list 1 |
Def | | compose_list(L) | [compose_list] | mb list 1 |
Def | | increasing(f;k) | [increasing] | mb basic |
Def | | {i..j } | [int_seg] | int 1 |
Def | | reducible(a) | [reducible] | num thy 1 |
Def | |    | [int_nzero] | int 1 |
Def | | Div(a;n;q) | [div_nrel] | int 2 |
Def | | i j < k | [lelt] | int 1 |
Def | | A B | [le] | core |
Def | | a b | [nequal] | core |
Def | | Dec(P) | [decidable] | core |
Def | | A | [not] | core |
Def | | filter(P;l) | [filter] | mb list 1 |
Def | | GCD(a;b;y) | [gcd_p] | num thy 1 |
Def | | a ~ b | [assoced] | num thy 1 |
Def | | b | a | [divides] | num thy 1 |
Def | | sum(f(x;y) | x < n; y < m) | [double_sum] | mb nat |
Def | | sum(f(x) | x < k) | [sum] | mb nat |
Def | | primrec(n;b;c) | [primrec] | mb nat |
Def | | rel_exp(T;R;n) | [rel_exp] | mb nat |
Def | | Case v = > case
cont | [switch_case] | prog 1 |
Def | | i= j | [eq_int] | bool 1 |
Def | | if b t else f fi | [ifthenelse] | bool 1 |
Def | | Y | [ycomb] | core |
Def | | P Q | [or] | core |
Def | | p  q | [bimplies] | bool 1 |
Def | | p  q | [bor] | bool 1 |
Def | | false | [bfalse] | bool 1 |
Def | | true | [btrue] | bool 1 |
Def | | as @ bs | [append] | list 1 |
Def | | A & B | [cand] | core |
Def | | nth_tl(n;as) | [nth_tl] | list 1 |
Def | | imax(a;b) | [imax] | int 2 |
Def | | i j | [le_int] | bool 1 |
Def | | firstn(n;as) | [firstn] | list 1 |
Def | | i < j | [lt_int] | bool 1 |
Def | | b | [assert] | bool 1 |
Def | | reduce(f;k;as) | [reduce] | list 1 |
Def | | 2of(t) | [pi2] | core |
Def | | 1of(t) | [pi1] | core |
Def | | p q | [band] | bool 1 |
Def | | InvFuns(A; B; f; g) | [inv_funs] | fun 1 |
Def | | f o g | [compose] | fun 1 |
Def | | True | [true] | core |
Def | | x f y | [infix_ap] | core |
Def | | Top | [top] | core |
Def | | Case ptn_int(x) = >
body(x)
cont | [case_ptn_int] | mb basic |
Def | | Case ptn_var(x) = >
body(x)
cont | [case_ptn_var] | mb basic |
Def | | tl(l) | [tl] | list 1 |
Def | | hd(l) | [hd] | list 1 |
Def | | inl(x) = >
body(x)
cont | [case_inl] | prog 1 |
Def | | inr(x) = >
body(x)
cont | [case_inr] | prog 1 |
Def | | ptn_con(T) | [ptn_con] | mb basic |
Def | | ptn_pr(x) | [ptn_pr] | mb basic |
Def | | Default = > body | [case_default] | prog 1 |
Def | | Case ptn_atom(x) = >
body(x)
cont | [case_ptn_atom] | mb basic |
Def | | Case(value)
body | [case] | prog 1 |
Def | | Case ptn_pr( < x, y > ) = >
body(x;y)
cont | [case_lbl_pair] | mb basic |
Def | | x= y Atom | [eq_atom] | bool 1 |
Def | | ptn_atom(x) | [ptn_atom] | mb basic |
Def | | Order(T;x,y.R(x;y)) | [order] | rel 1 |
Def | | Trans x,y:T. E(x;y) | [trans] | rel 1 |
Def | | Sym x,y:T. E(x;y) | [sym] | rel 1 |
Def | | Refl(T;x,y.E(x;y)) | [refl] | rel 1 |
Def | | P  Q | [iff] | core |
Def | | AntiSym(T;x,y.R(x;y)) | [anti_sym] | rel 1 |
Def | | Connex(T;x,y.R(x;y)) | [connex] | rel 1 |
Def | | x:T. b(x) | [tlambda] | fun 1 |
Def | | mapcons(f;as) | [mapcons] | list 1 |
Def | | Id | [tidentity] | fun 1 |
Def | | Id | [identity] | fun 1 |
Def | | Surj(A; B; f) | [surject] | fun 1 |
Def | | Inj(A; B; f) | [inject] | fun 1 |
Def | | tree_con(E;T) | [tree_con] | mb tree |
Def | | Case tree_leaf(x) = >
body(x)
cont | [case_tree_leaf] | mb tree |
Def | | Case x;y = >
body(x;y)
cont | [case_node] | mb tree |
Def | | tree_node(x) | [tree_node] | mb tree |
Def | | < < "a", b > , c, 1 > | [pattern1] | prog 1 |
Def | |  | [bool] | bool 1 |
Def | | EndSwitch | [switch_done] | prog 1 |
Def | | enum1_el3 | [enum1_el3] | prog 1 |
Def | | enum1_el2 | [enum1_el2] | prog 1 |
Def | | enum1_el1 | [enum1_el1] | prog 1 |
Def | | Switch(t)
b | [switch] | prog 1 |
Def | | Unit | [unit] | core |
Def | | {T} | [guard] | core |
Def | |  | [it] | core |
Def | | False | [false] | core |
Def | |  b | [bnot] | bool 1 |
Def | | S T | [subtype] | core |
Def | | Prop | [prop] | core |
Def | | P  Q | [rev_implies] | core |
Def | | T | [squash] | core |