constants.txt

absurd
acc.cases_on
acc.rec
and
and.cases_on
and.elim_left
and.elim_right
and.intro
and.rec
auto_param
bin_tree.empty
bin_tree.leaf
bin_tree.node
bit0
bit1
bool
bool.ff
bool.tt
cast
cast_heq
char
char.mk
char.ne_of_vne
char.of_nat
char.of_nat_ne_of_ne
coe
coe_fn
coe_sort
coe_to_lift
combinator.K
congr
congr_arg
congr_fun
decidable
decidable.to_bool
dite
empty
eq
eq.cases_on
eq.drec
eq.mp
eq.mpr
eq.rec
eq.refl
eq.subst
eq.symm
eq.trans
eq_false_intro
eq_of_heq
eq_rec_heq
eq_self_iff_true
eq_true_intro
Exists
expr
expr.subst
false
false.rec
false_of_true_eq_false
fin.mk
fin.ne_of_vne
forall_congr
forall_congr_eq
forall_not_of_not_exists
format
funext
has_add
has_add.add
has_andthen.andthen
has_bind.and_then
has_bind.seq
has_coe_t
has_coe_to_fun
has_coe_to_sort
has_div.div
has_emptyc.emptyc
has_insert.insert
has_neg.neg
has_one
has_one.one
has_orelse.orelse
has_repr
has_sep.sep
has_singleton.singleton
has_sizeof
has_sizeof.mk
has_sub.sub
has_to_format
has_well_founded
has_well_founded.r
has_well_founded.wf
has_zero
has_zero.zero
heq
heq.refl
heq.symm
heq.trans
heq_of_eq
hole_command
id
id_delta
id_rhs
if_neg
if_pos
iff
iff.intro
iff.mp
iff.mpr
iff.refl
iff.symm
iff.trans
iff_false_intro
iff_true_intro
imp_congr
imp_congr_ctx
imp_congr_ctx_eq
imp_congr_eq
implies
implies_of_if_neg
implies_of_if_pos
int
int.bit0_nonneg
int.bit0_pos
int.bit1_nonneg
int.bit1_pos
int.nat_abs_bit0_step
int.nat_abs_bit1_nonneg_step
int.nat_abs_one
int.nat_abs_zero
int.ne_neg_of_ne
int.ne_neg_of_pos
int.ne_of_nat_ne_nonneg_case
int.neg_ne_of_pos
int.neg_ne_zero_of_ne
int.one_nonneg
int.one_pos
int.zero_ne_neg_of_ne
int.zero_nonneg
interactive.executor
interactive.param_desc
interactive.parse
io
io_core
io_rand_nat
is_associative
is_associative.assoc
is_commutative
is_commutative.comm
is_valid_char_range_1
is_valid_char_range_2
ite
lean.parser
lean.parser.pexpr
lean.parser.reflectable.expr
lean.parser.tk
left_comm
list
list.cons
list.nil
match_failed
monad
monad_fail
monad_from_pure_bind
monad_io_environment_impl
monad_io_file_system_impl
monad_io_impl
monad_io_net_system_impl
monad_io_process_impl
monad_io_random_impl
monad_io_terminal_impl
name.anonymous
name.mk_numeral
name.mk_string
nat
nat.add
nat.bit0_lt
nat.bit0_lt_bit1
nat.bit0_ne
nat.bit0_ne_bit1
nat.bit0_ne_one
nat.bit0_ne_zero
nat.bit1_lt
nat.bit1_lt_bit0
nat.bit1_ne
nat.bit1_ne_bit0
nat.bit1_ne_one
nat.bit1_ne_zero
nat.cases_on
nat.has_add
nat.has_one
nat.has_zero
nat.le_of_lt
nat.le_refl
nat.one_lt_bit0
nat.one_lt_bit1
nat.one_ne_bit0
nat.one_ne_bit1
nat.one_ne_zero
nat.succ
nat.zero
nat.zero_lt_bit0
nat.zero_lt_bit1
nat.zero_lt_one
nat.zero_ne_bit0
nat.zero_ne_bit1
nat.zero_ne_one
ne
neq_of_not_iff
not
not_of_eq_false
of_eq_true
opt_param
or
out_param
pprod
pprod.fst
pprod.mk
pprod.snd
prod.mk
propext
psigma
psigma.cases_on
psigma.fst
psigma.mk
psigma.snd
psum
psum.cases_on
psum.inl
psum.inr
punit
punit.cases_on
punit.star
quot.lift
quot.mk
reflected
reflected.subst
repr
rfl
scope_trace
set_of
sizeof
string
string.empty
string.empty_ne_str
string.str
string.str_ne_empty
string.str_ne_str_left
string.str_ne_str_right
subsingleton
subsingleton.elim
subsingleton.helim
subtype
subtype.mk
subtype.rec
subtype.val
tactic
tactic.mk_inj_eq
tactic.triv
tactic.try
thunk
to_fmt
to_pexpr
trans_rel_left
trans_rel_right
true
true.intro
true_eq_false_of_false
unification_hint
unification_hint.mk
unit
unit.star
user_attribute
user_attribute.parse_reflect
vm_monitor
well_founded.fix
well_founded.fix_eq
well_founded_tactics
well_founded_tactics.dec_tac
well_founded_tactics.default
well_founded_tactics.rel_tac
widget.term_goal_widget