-
-
Save bryangingechen/6c2f397b14d756c3c7f72440cd9b4816 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import tactic.lint | |
| /- Checking 4868 declarations (plus 7002 automatically generated ones) in all imported files (including this one) -/ | |
| /- The `def_lemma` linter reports: -/ | |
| /- INCORRECT DEF/LEMMA: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/order.lean | |
| #print lt.trans /- is a def, should be a lemma/theorem -/ | |
| #print gt.trans /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/classical.lean | |
| #print classical.indefinite_description /- is a lemma/theorem, should be a def -/ | |
| #print classical.strong_indefinite_description /- is a lemma/theorem, should be a def -/ | |
| #print classical.eq_true_or_eq_false /- is a def, should be a lemma/theorem -/ | |
| #print classical.by_cases /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/core.lean | |
| #print and.elim_left /- is a def, should be a lemma/theorem -/ | |
| #print and.elim_right /- is a def, should be a lemma/theorem -/ | |
| #print rfl /- is a def, should be a lemma/theorem -/ | |
| #print heq.rfl /- is a def, should be a lemma/theorem -/ | |
| #print or.intro_left /- is a def, should be a lemma/theorem -/ | |
| #print or.intro_right /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/basic.lean | |
| #print nat.le_refl /- is a def, should be a lemma/theorem -/ | |
| #print nat.succ_pos /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/lemmas.lean | |
| #print nat.lt.step /- is a def, should be a lemma/theorem -/ | |
| #print nat.lt.base /- is a def, should be a lemma/theorem -/ | |
| #print nat.discriminate /- is a lemma/theorem, should be a def -/ | |
| #print nat.two_step_induction /- is a lemma/theorem, should be a def -/ | |
| #print nat.sub_induction /- is a lemma/theorem, should be a def -/ | |
| #print nat.one_pos /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/quot.lean | |
| #print quotient.sound /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/sigma/lex.lean | |
| #print psigma.lex_accessible /- is a def, should be a lemma/theorem -/ | |
| #print psigma.lex_wf /- is a def, should be a lemma/theorem -/ | |
| #print psigma.lex_ndep_wf /- is a def, should be a lemma/theorem -/ | |
| #print psigma.rev_lex_accessible /- is a def, should be a lemma/theorem -/ | |
| #print psigma.rev_lex_wf /- is a def, should be a lemma/theorem -/ | |
| #print psigma.skip_left_wf /- is a def, should be a lemma/theorem -/ | |
| #print psigma.mk_skip_left /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/subtype/basic.lean | |
| #print subtype.exists_of_subtype /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/function.lean | |
| #print function.right_inverse.id /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print trivial /- is a def, should be a lemma/theorem -/ | |
| #print heq.elim /- is a lemma/theorem, should be a def -/ | |
| #print type_eq_of_heq /- is a def, should be a lemma/theorem -/ | |
| #print and.symm /- is a def, should be a lemma/theorem -/ | |
| #print not_not_em /- is a def, should be a lemma/theorem -/ | |
| #print or.symm /- is a def, should be a lemma/theorem -/ | |
| #print not_not_not_iff /- is a def, should be a lemma/theorem -/ | |
| #print not_true_iff /- is a def, should be a lemma/theorem -/ | |
| #print and_implies /- is a def, should be a lemma/theorem -/ | |
| #print or.resolve_left /- is a def, should be a lemma/theorem -/ | |
| #print or.neg_resolve_left /- is a def, should be a lemma/theorem -/ | |
| #print or.resolve_right /- is a def, should be a lemma/theorem -/ | |
| #print or.neg_resolve_right /- is a def, should be a lemma/theorem -/ | |
| #print exists.intro /- is a def, should be a lemma/theorem -/ | |
| #print nonempty.elim /- is a def, should be a lemma/theorem -/ | |
| #print subsingleton.elim /- is a def, should be a lemma/theorem -/ | |
| #print subsingleton.helim /- is a def, should be a lemma/theorem -/ | |
| #print of_as_true /- is a def, should be a lemma/theorem -/ | |
| #print mk_equivalence /- is a def, should be a lemma/theorem -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/wf.lean | |
| #print acc.inv /- is a def, should be a lemma/theorem -/ | |
| #print well_founded.apply /- is a def, should be a lemma/theorem -/ | |
| #print well_founded.recursion /- is a lemma/theorem, should be a def -/ | |
| #print empty_wf /- is a def, should be a lemma/theorem -/ | |
| #print subrelation.accessible /- is a def, should be a lemma/theorem -/ | |
| #print subrelation.wf /- is a def, should be a lemma/theorem -/ | |
| #print inv_image.accessible /- is a def, should be a lemma/theorem -/ | |
| #print inv_image.wf /- is a def, should be a lemma/theorem -/ | |
| #print tc.accessible /- is a def, should be a lemma/theorem -/ | |
| #print tc.wf /- is a def, should be a lemma/theorem -/ | |
| #print nat.lt_wf /- is a def, should be a lemma/theorem -/ | |
| #print measure_wf /- is a def, should be a lemma/theorem -/ | |
| #print sizeof_measure_wf /- is a def, should be a lemma/theorem -/ | |
| #print prod.lex_accessible /- is a def, should be a lemma/theorem -/ | |
| #print prod.lex_wf /- is a def, should be a lemma/theorem -/ | |
| #print prod.rprod_sub_lex /- is a def, should be a lemma/theorem -/ | |
| #print prod.rprod_wf /- is a def, should be a lemma/theorem -/ | |
| /- The `doc_blame` linter reports: -/ | |
| /- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/ | |
| -- | |
| #print quot.lift /- constant missing doc string -/ | |
| #print quot /- constant missing doc string -/ | |
| #print quot.ind /- constant missing doc string -/ | |
| #print quot.mk /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/classes.lean | |
| #print is_symm_op /- constant missing doc string -/ | |
| #print is_commutative /- constant missing doc string -/ | |
| #print is_associative /- constant missing doc string -/ | |
| #print is_left_id /- constant missing doc string -/ | |
| #print is_right_id /- constant missing doc string -/ | |
| #print is_left_null /- constant missing doc string -/ | |
| #print is_right_null /- constant missing doc string -/ | |
| #print is_left_cancel /- constant missing doc string -/ | |
| #print is_right_cancel /- constant missing doc string -/ | |
| #print is_idempotent /- constant missing doc string -/ | |
| #print is_left_distrib /- constant missing doc string -/ | |
| #print is_right_distrib /- constant missing doc string -/ | |
| #print is_left_inv /- constant missing doc string -/ | |
| #print is_right_inv /- constant missing doc string -/ | |
| #print is_cond_left_inv /- constant missing doc string -/ | |
| #print is_cond_right_inv /- constant missing doc string -/ | |
| #print is_distinct /- constant missing doc string -/ | |
| #print is_irrefl /- constant missing doc string -/ | |
| #print is_refl /- constant missing doc string -/ | |
| #print is_symm /- constant missing doc string -/ | |
| #print is_asymm /- constant missing doc string -/ | |
| #print is_antisymm /- constant missing doc string -/ | |
| #print is_trans /- constant missing doc string -/ | |
| #print is_total /- constant missing doc string -/ | |
| #print is_preorder /- constant missing doc string -/ | |
| #print is_total_preorder /- constant missing doc string -/ | |
| #print is_partial_order /- constant missing doc string -/ | |
| #print is_linear_order /- constant missing doc string -/ | |
| #print is_equiv /- constant missing doc string -/ | |
| #print is_per /- constant missing doc string -/ | |
| #print is_strict_order /- constant missing doc string -/ | |
| #print is_incomp_trans /- constant missing doc string -/ | |
| #print is_strict_weak_order /- constant missing doc string -/ | |
| #print is_trichotomous /- constant missing doc string -/ | |
| #print is_strict_total_order /- constant missing doc string -/ | |
| #print strict_weak_order.equiv /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/functions.lean | |
| #print min /- def missing doc string -/ | |
| #print max /- def missing doc string -/ | |
| #print tactic.interactive.min_tac /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/order.lean | |
| #print lt.trans /- def missing doc string -/ | |
| #print gt.trans /- def missing doc string -/ | |
| #print decidable_linear_order /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/classical.lean | |
| #print classical.some /- def missing doc string -/ | |
| #print classical.inhabited_of_nonempty /- def missing doc string -/ | |
| #print classical.inhabited_of_exists /- def missing doc string -/ | |
| #print classical.prop_decidable /- def missing doc string -/ | |
| #print classical.decidable_inhabited /- def missing doc string -/ | |
| #print classical.type_decidable_eq /- def missing doc string -/ | |
| #print classical.type_decidable /- def missing doc string -/ | |
| #print classical.epsilon /- def missing doc string -/ | |
| #print classical.eq_true_or_eq_false /- def missing doc string -/ | |
| #print classical.by_cases /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/coe.lean | |
| #print has_coe /- constant missing doc string -/ | |
| #print has_coe_to_fun /- constant missing doc string -/ | |
| #print has_coe_to_sort /- constant missing doc string -/ | |
| #print lift /- def missing doc string -/ | |
| #print lift_t /- def missing doc string -/ | |
| #print coe_b /- def missing doc string -/ | |
| #print coe_t /- def missing doc string -/ | |
| #print coe_fn_b /- def missing doc string -/ | |
| #print coe /- def missing doc string -/ | |
| #print coe_fn /- def missing doc string -/ | |
| #print coe_sort /- def missing doc string -/ | |
| #print has_coe_t_aux /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/alternative.lean | |
| #print has_orelse /- constant missing doc string -/ | |
| #print alternative /- constant missing doc string -/ | |
| #print failure /- def missing doc string -/ | |
| #print assert /- def missing doc string -/ | |
| #print guardb /- def missing doc string -/ | |
| #print optional /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/applicative.lean | |
| #print has_pure /- constant missing doc string -/ | |
| #print has_seq /- constant missing doc string -/ | |
| #print has_seq_left /- constant missing doc string -/ | |
| #print has_seq_right /- constant missing doc string -/ | |
| #print applicative /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/combinators.lean | |
| #print list.mmap /- def missing doc string -/ | |
| #print list.mmap' /- def missing doc string -/ | |
| #print mjoin /- def missing doc string -/ | |
| #print list.mfilter /- def missing doc string -/ | |
| #print list.mfoldl /- def missing doc string -/ | |
| #print list.mfoldr /- def missing doc string -/ | |
| #print list.mfirst /- def missing doc string -/ | |
| #print when /- def missing doc string -/ | |
| #print mcond /- def missing doc string -/ | |
| #print mwhen /- def missing doc string -/ | |
| #print monad.mapm /- def missing doc string -/ | |
| #print monad.mapm' /- def missing doc string -/ | |
| #print monad.join /- def missing doc string -/ | |
| #print monad.filter /- def missing doc string -/ | |
| #print monad.foldl /- def missing doc string -/ | |
| #print monad.cond /- def missing doc string -/ | |
| #print monad.sequence /- def missing doc string -/ | |
| #print monad.sequence' /- def missing doc string -/ | |
| #print monad.whenb /- def missing doc string -/ | |
| #print monad.unlessb /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print except /- constant missing doc string -/ | |
| #print except.return /- def missing doc string -/ | |
| #print except.map /- def missing doc string -/ | |
| #print except.map_error /- def missing doc string -/ | |
| #print except.bind /- def missing doc string -/ | |
| #print except.to_bool /- def missing doc string -/ | |
| #print except.to_option /- def missing doc string -/ | |
| #print except_t /- constant missing doc string -/ | |
| #print except_t.return /- def missing doc string -/ | |
| #print except_t.bind_cont /- def missing doc string -/ | |
| #print except_t.bind /- def missing doc string -/ | |
| #print except_t.lift /- def missing doc string -/ | |
| #print except_t.catch /- def missing doc string -/ | |
| #print except_t.monad_map /- def missing doc string -/ | |
| #print except_t.adapt /- def missing doc string -/ | |
| #print monad_except.orelse /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/functor.lean | |
| #print functor /- constant missing doc string -/ | |
| #print functor.map_const_rev /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/id.lean | |
| #print id_bind /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/lawful.lean | |
| #print control_laws_tac /- def missing doc string -/ | |
| #print is_lawful_functor /- constant missing doc string -/ | |
| #print is_lawful_applicative /- constant missing doc string -/ | |
| #print is_lawful_monad /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad.lean | |
| #print has_bind /- constant missing doc string -/ | |
| #print has_bind.and_then /- def missing doc string -/ | |
| #print monad /- constant missing doc string -/ | |
| #print return /- def missing doc string -/ | |
| #print has_bind.seq /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad_fail.lean | |
| #print monad_fail /- constant missing doc string -/ | |
| #print match_failed /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/option.lean | |
| #print option_t /- constant missing doc string -/ | |
| #print option_t.bind_cont /- def missing doc string -/ | |
| #print option_t.bind /- def missing doc string -/ | |
| #print option_t.pure /- def missing doc string -/ | |
| #print option_t.orelse /- def missing doc string -/ | |
| #print option_t.fail /- def missing doc string -/ | |
| #print option_t.of_option /- def missing doc string -/ | |
| #print option_t.lift /- def missing doc string -/ | |
| #print option_t.monad_map /- def missing doc string -/ | |
| #print option_t.catch /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print reader /- def missing doc string -/ | |
| #print reader_t.read /- def missing doc string -/ | |
| #print reader_t.pure /- def missing doc string -/ | |
| #print reader_t.bind /- def missing doc string -/ | |
| #print reader_t.lift /- def missing doc string -/ | |
| #print reader_t.monad_map /- def missing doc string -/ | |
| #print reader_t.adapt /- def missing doc string -/ | |
| #print reader_t.orelse /- def missing doc string -/ | |
| #print reader_t.failure /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print state_t /- constant missing doc string -/ | |
| #print state /- def missing doc string -/ | |
| #print state_t.pure /- def missing doc string -/ | |
| #print state_t.bind /- def missing doc string -/ | |
| #print state_t.orelse /- def missing doc string -/ | |
| #print state_t.failure /- def missing doc string -/ | |
| #print state_t.get /- def missing doc string -/ | |
| #print state_t.put /- def missing doc string -/ | |
| #print state_t.modify /- def missing doc string -/ | |
| #print state_t.lift /- def missing doc string -/ | |
| #print state_t.monad_map /- def missing doc string -/ | |
| #print state_t.adapt /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/core.lean | |
| #print id_rhs /- def missing doc string -/ | |
| #print punit /- constant missing doc string -/ | |
| #print unit.star /- def missing doc string -/ | |
| #print true /- constant missing doc string -/ | |
| #print false /- constant missing doc string -/ | |
| #print empty /- constant missing doc string -/ | |
| #print not /- def missing doc string -/ | |
| #print eq /- constant missing doc string -/ | |
| #print prod /- constant missing doc string -/ | |
| #print and /- constant missing doc string -/ | |
| #print and.elim_left /- def missing doc string -/ | |
| #print and.elim_right /- def missing doc string -/ | |
| #print rfl /- def missing doc string -/ | |
| #print heq.rfl /- def missing doc string -/ | |
| #print sum /- constant missing doc string -/ | |
| #print psum /- constant missing doc string -/ | |
| #print or /- constant missing doc string -/ | |
| #print or.intro_left /- def missing doc string -/ | |
| #print or.intro_right /- def missing doc string -/ | |
| #print sigma /- constant missing doc string -/ | |
| #print psigma /- constant missing doc string -/ | |
| #print bool /- constant missing doc string -/ | |
| #print subtype /- constant missing doc string -/ | |
| #print decidable /- constant missing doc string -/ | |
| #print decidable_pred /- def missing doc string -/ | |
| #print decidable_rel /- def missing doc string -/ | |
| #print decidable_eq /- def missing doc string -/ | |
| #print option /- constant missing doc string -/ | |
| #print list /- constant missing doc string -/ | |
| #print nat /- constant missing doc string -/ | |
| #print unification_constraint /- constant missing doc string -/ | |
| #print unification_hint /- constant missing doc string -/ | |
| #print has_zero /- constant missing doc string -/ | |
| #print has_one /- constant missing doc string -/ | |
| #print has_add /- constant missing doc string -/ | |
| #print has_mul /- constant missing doc string -/ | |
| #print has_inv /- constant missing doc string -/ | |
| #print has_neg /- constant missing doc string -/ | |
| #print has_sub /- constant missing doc string -/ | |
| #print has_div /- constant missing doc string -/ | |
| #print has_dvd /- constant missing doc string -/ | |
| #print has_mod /- constant missing doc string -/ | |
| #print has_le /- constant missing doc string -/ | |
| #print has_lt /- constant missing doc string -/ | |
| #print has_append /- constant missing doc string -/ | |
| #print has_andthen /- constant missing doc string -/ | |
| #print has_union /- constant missing doc string -/ | |
| #print has_inter /- constant missing doc string -/ | |
| #print has_sdiff /- constant missing doc string -/ | |
| #print has_equiv /- constant missing doc string -/ | |
| #print has_subset /- constant missing doc string -/ | |
| #print has_ssubset /- constant missing doc string -/ | |
| #print has_emptyc /- constant missing doc string -/ | |
| #print has_insert /- constant missing doc string -/ | |
| #print has_singleton /- constant missing doc string -/ | |
| #print has_sep /- constant missing doc string -/ | |
| #print has_mem /- constant missing doc string -/ | |
| #print has_pow /- constant missing doc string -/ | |
| #print ge /- def missing doc string -/ | |
| #print gt /- def missing doc string -/ | |
| #print superset /- def missing doc string -/ | |
| #print ssuperset /- def missing doc string -/ | |
| #print bit0 /- def missing doc string -/ | |
| #print bit1 /- def missing doc string -/ | |
| #print is_lawful_singleton /- constant missing doc string -/ | |
| #print nat.add /- def missing doc string -/ | |
| #print std.priority.default /- def missing doc string -/ | |
| #print std.priority.max /- def missing doc string -/ | |
| #print nat.prio /- def missing doc string -/ | |
| #print std.prec.max /- def missing doc string -/ | |
| #print std.prec.arrow /- def missing doc string -/ | |
| #print std.prec.max_plus /- def missing doc string -/ | |
| #print has_sizeof /- constant missing doc string -/ | |
| #print sizeof /- def missing doc string -/ | |
| #print default.sizeof /- def missing doc string -/ | |
| #print combinator.I /- def missing doc string -/ | |
| #print combinator.K /- def missing doc string -/ | |
| #print combinator.S /- def missing doc string -/ | |
| #print add_succ_defeq_succ_add_hint /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/array/basic.lean | |
| #print d_array.iterate_aux /- def missing doc string -/ | |
| #print d_array.map /- def missing doc string -/ | |
| #print d_array.map₂ /- def missing doc string -/ | |
| #print d_array.foldl /- def missing doc string -/ | |
| #print d_array.rev_iterate_aux /- def missing doc string -/ | |
| #print d_array.rev_iterate /- def missing doc string -/ | |
| #print d_array.beq_aux /- def missing doc string -/ | |
| #print array.nil /- def missing doc string -/ | |
| #print array.read /- def missing doc string -/ | |
| #print array.write /- def missing doc string -/ | |
| #print array.map₂ /- def missing doc string -/ | |
| #print array.foldl /- def missing doc string -/ | |
| #print array.rev_list /- def missing doc string -/ | |
| #print array.rev_iterate /- def missing doc string -/ | |
| #print array.rev_foldl /- def missing doc string -/ | |
| #print array.to_list /- def missing doc string -/ | |
| #print array.mem /- def missing doc string -/ | |
| #print array.read' /- def missing doc string -/ | |
| #print array.write' /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/array/slice.lean | |
| #print array.slice /- def missing doc string -/ | |
| #print array.take /- def missing doc string -/ | |
| #print array.drop /- def missing doc string -/ | |
| #print array.take_right /- def missing doc string -/ | |
| #print array.reverse /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/bool/basic.lean | |
| #print cond /- def missing doc string -/ | |
| #print bor /- def missing doc string -/ | |
| #print band /- def missing doc string -/ | |
| #print bnot /- def missing doc string -/ | |
| #print bxor /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/char/basic.lean | |
| #print is_valid_char /- def missing doc string -/ | |
| #print char.lt /- def missing doc string -/ | |
| #print char.le /- def missing doc string -/ | |
| #print char.of_nat /- def missing doc string -/ | |
| #print char.to_nat /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/char/classes.lean | |
| #print char.is_whitespace /- def missing doc string -/ | |
| #print char.is_upper /- def missing doc string -/ | |
| #print char.is_lower /- def missing doc string -/ | |
| #print char.is_alpha /- def missing doc string -/ | |
| #print char.is_digit /- def missing doc string -/ | |
| #print char.is_alphanum /- def missing doc string -/ | |
| #print char.is_punctuation /- def missing doc string -/ | |
| #print char.to_lower /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/fin/basic.lean | |
| #print fin /- constant missing doc string -/ | |
| #print fin.lt /- def missing doc string -/ | |
| #print fin.le /- def missing doc string -/ | |
| #print fin.elim0 /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/fin/ops.lean | |
| #print fin.succ /- def missing doc string -/ | |
| #print fin.of_nat /- def missing doc string -/ | |
| #print fin.add /- def missing doc string -/ | |
| #print fin.mul /- def missing doc string -/ | |
| #print fin.sub /- def missing doc string -/ | |
| #print fin.mod /- def missing doc string -/ | |
| #print fin.div /- def missing doc string -/ | |
| #print fin.pred /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/basic.lean | |
| #print int /- constant missing doc string -/ | |
| #print int.repr /- def missing doc string -/ | |
| #print int.zero /- def missing doc string -/ | |
| #print int.one /- def missing doc string -/ | |
| #print int.neg_of_nat /- def missing doc string -/ | |
| #print int.sub_nat_nat /- def missing doc string -/ | |
| #print int.neg /- def missing doc string -/ | |
| #print int.add /- def missing doc string -/ | |
| #print int.mul /- def missing doc string -/ | |
| #print int.sub /- def missing doc string -/ | |
| #print int.nat_abs /- def missing doc string -/ | |
| #print int.sign /- def missing doc string -/ | |
| #print int.div /- def missing doc string -/ | |
| #print int.mod /- def missing doc string -/ | |
| #print int.fdiv /- def missing doc string -/ | |
| #print int.fmod /- def missing doc string -/ | |
| #print int.quot /- def missing doc string -/ | |
| #print int.rem /- def missing doc string -/ | |
| #print int.gcd /- def missing doc string -/ | |
| #print int.to_nat /- def missing doc string -/ | |
| #print int.nat_mod /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/bitwise.lean | |
| #print int.div2 /- def missing doc string -/ | |
| #print int.bodd /- def missing doc string -/ | |
| #print int.bit /- def missing doc string -/ | |
| #print int.test_bit /- def missing doc string -/ | |
| #print int.nat_bitwise /- def missing doc string -/ | |
| #print int.bitwise /- def missing doc string -/ | |
| #print int.lnot /- def missing doc string -/ | |
| #print int.lor /- def missing doc string -/ | |
| #print int.land /- def missing doc string -/ | |
| #print int.ldiff /- def missing doc string -/ | |
| #print int.lxor /- def missing doc string -/ | |
| #print int.shiftl /- def missing doc string -/ | |
| #print int.shiftr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/order.lean | |
| #print int.le /- def missing doc string -/ | |
| #print int.lt /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/basic.lean | |
| #print list.has_dec_eq /- def missing doc string -/ | |
| #print list.append /- def missing doc string -/ | |
| #print list.mem /- def missing doc string -/ | |
| #print list.erase /- def missing doc string -/ | |
| #print list.bag_inter /- def missing doc string -/ | |
| #print list.diff /- def missing doc string -/ | |
| #print list.length /- def missing doc string -/ | |
| #print list.empty /- def missing doc string -/ | |
| #print list.nth /- def missing doc string -/ | |
| #print list.nth_le /- def missing doc string -/ | |
| #print list.head /- def missing doc string -/ | |
| #print list.tail /- def missing doc string -/ | |
| #print list.reverse_core /- def missing doc string -/ | |
| #print list.reverse /- def missing doc string -/ | |
| #print list.map /- def missing doc string -/ | |
| #print list.map₂ /- def missing doc string -/ | |
| #print list.join /- def missing doc string -/ | |
| #print list.filter_map /- def missing doc string -/ | |
| #print list.filter /- def missing doc string -/ | |
| #print list.partition /- def missing doc string -/ | |
| #print list.drop_while /- def missing doc string -/ | |
| #print list.span /- def missing doc string -/ | |
| #print list.find_index /- def missing doc string -/ | |
| #print list.index_of /- def missing doc string -/ | |
| #print list.remove_all /- def missing doc string -/ | |
| #print list.update_nth /- def missing doc string -/ | |
| #print list.remove_nth /- def missing doc string -/ | |
| #print list.drop /- def missing doc string -/ | |
| #print list.take /- def missing doc string -/ | |
| #print list.foldl /- def missing doc string -/ | |
| #print list.foldr /- def missing doc string -/ | |
| #print list.any /- def missing doc string -/ | |
| #print list.all /- def missing doc string -/ | |
| #print list.bor /- def missing doc string -/ | |
| #print list.band /- def missing doc string -/ | |
| #print list.zip_with /- def missing doc string -/ | |
| #print list.zip /- def missing doc string -/ | |
| #print list.unzip /- def missing doc string -/ | |
| #print list.insert /- def missing doc string -/ | |
| #print list.union /- def missing doc string -/ | |
| #print list.inter /- def missing doc string -/ | |
| #print list.repeat /- def missing doc string -/ | |
| #print list.range_core /- def missing doc string -/ | |
| #print list.range /- def missing doc string -/ | |
| #print list.iota /- def missing doc string -/ | |
| #print list.enum_from /- def missing doc string -/ | |
| #print list.enum /- def missing doc string -/ | |
| #print list.last /- def missing doc string -/ | |
| #print list.ilast /- def missing doc string -/ | |
| #print list.init /- def missing doc string -/ | |
| #print list.intersperse /- def missing doc string -/ | |
| #print list.intercalate /- def missing doc string -/ | |
| #print list.bind /- def missing doc string -/ | |
| #print list.ret /- def missing doc string -/ | |
| #print list.lt /- def missing doc string -/ | |
| #print list.le /- def missing doc string -/ | |
| #print bin_tree.to_list /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/lemmas.lean | |
| #print list.subset /- def missing doc string -/ | |
| #print list.sublist /- constant missing doc string -/ | |
| #print list.map_accumr /- def missing doc string -/ | |
| #print list.map_accumr₂ /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/qsort.lean | |
| #print list.qsort.F /- def missing doc string -/ | |
| #print list.qsort /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/basic.lean | |
| #print nat.less_than_or_equal /- constant missing doc string -/ | |
| #print nat.le /- def missing doc string -/ | |
| #print nat.lt /- def missing doc string -/ | |
| #print nat.pred /- def missing doc string -/ | |
| #print nat.sub /- def missing doc string -/ | |
| #print nat.mul /- def missing doc string -/ | |
| #print nat.repeat /- def missing doc string -/ | |
| #print nat.le_refl /- def missing doc string -/ | |
| #print nat.succ_pos /- def missing doc string -/ | |
| #print nat.pow /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/bitwise.lean | |
| #print nat.bodd_div2 /- def missing doc string -/ | |
| #print nat.div2 /- def missing doc string -/ | |
| #print nat.bodd /- def missing doc string -/ | |
| #print nat.bit /- def missing doc string -/ | |
| #print nat.bit_cases_on /- def missing doc string -/ | |
| #print nat.shiftl' /- def missing doc string -/ | |
| #print nat.shiftl /- def missing doc string -/ | |
| #print nat.shiftr /- def missing doc string -/ | |
| #print nat.test_bit /- def missing doc string -/ | |
| #print nat.binary_rec /- def missing doc string -/ | |
| #print nat.size /- def missing doc string -/ | |
| #print nat.bits /- def missing doc string -/ | |
| #print nat.bitwise /- def missing doc string -/ | |
| #print nat.lor /- def missing doc string -/ | |
| #print nat.land /- def missing doc string -/ | |
| #print nat.ldiff /- def missing doc string -/ | |
| #print nat.lxor /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/div.lean | |
| #print nat.div /- def missing doc string -/ | |
| #print nat.mod /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/gcd.lean | |
| #print nat.gcd /- def missing doc string -/ | |
| #print nat.lcm /- def missing doc string -/ | |
| #print nat.coprime /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/lemmas.lean | |
| #print nat.lt.step /- def missing doc string -/ | |
| #print nat.lt.base /- def missing doc string -/ | |
| #print nat.strong_rec_on /- def missing doc string -/ | |
| #print nat.iterate /- def missing doc string -/ | |
| #print nat.lt_ge_by_cases /- def missing doc string -/ | |
| #print nat.lt_by_cases /- def missing doc string -/ | |
| #print nat.one_pos /- def missing doc string -/ | |
| #print nat.find_x /- def missing doc string -/ | |
| #print nat.find /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/option/basic.lean | |
| #print option.to_monad /- def missing doc string -/ | |
| #print option.get_or_else /- def missing doc string -/ | |
| #print option.is_some /- def missing doc string -/ | |
| #print option.is_none /- def missing doc string -/ | |
| #print option.get /- def missing doc string -/ | |
| #print option.rhoare /- def missing doc string -/ | |
| #print option.lhoare /- def missing doc string -/ | |
| #print option.bind /- def missing doc string -/ | |
| #print option.map /- def missing doc string -/ | |
| #print option.orelse /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/ordering/basic.lean | |
| #print ordering /- constant missing doc string -/ | |
| #print ordering.swap /- def missing doc string -/ | |
| #print ordering.or_else /- def missing doc string -/ | |
| #print cmp_using /- def missing doc string -/ | |
| #print cmp /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/prod.lean | |
| #print prod.map /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/quot.lean | |
| #print quot.sound /- constant missing doc string -/ | |
| #print quot.lift_on /- def missing doc string -/ | |
| #print quot.indep /- def missing doc string -/ | |
| #print quot.rec /- def missing doc string -/ | |
| #print quot.rec_on /- def missing doc string -/ | |
| #print quot.rec_on_subsingleton /- def missing doc string -/ | |
| #print quot.hrec_on /- def missing doc string -/ | |
| #print quotient /- def missing doc string -/ | |
| #print quotient.mk /- def missing doc string -/ | |
| #print quotient.sound /- def missing doc string -/ | |
| #print quotient.lift /- def missing doc string -/ | |
| #print quotient.lift_on /- def missing doc string -/ | |
| #print quotient.rec /- def missing doc string -/ | |
| #print quotient.rec_on /- def missing doc string -/ | |
| #print quotient.rec_on_subsingleton /- def missing doc string -/ | |
| #print quotient.hrec_on /- def missing doc string -/ | |
| #print quotient.lift₂ /- def missing doc string -/ | |
| #print quotient.lift_on₂ /- def missing doc string -/ | |
| #print quotient.rec_on_subsingleton₂ /- def missing doc string -/ | |
| #print eqv_gen /- constant missing doc string -/ | |
| #print eqv_gen.setoid /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/rbmap/basic.lean | |
| #print rbmap_lt /- def missing doc string -/ | |
| #print rbmap /- def missing doc string -/ | |
| #print mk_rbmap /- def missing doc string -/ | |
| #print rbmap.empty /- def missing doc string -/ | |
| #print rbmap.to_list /- def missing doc string -/ | |
| #print rbmap.min /- def missing doc string -/ | |
| #print rbmap.max /- def missing doc string -/ | |
| #print rbmap.fold /- def missing doc string -/ | |
| #print rbmap.rev_fold /- def missing doc string -/ | |
| #print rbmap.mem /- def missing doc string -/ | |
| #print rbmap.rbmap_lt_dec /- def missing doc string -/ | |
| #print rbmap.insert /- def missing doc string -/ | |
| #print rbmap.find_entry /- def missing doc string -/ | |
| #print rbmap.to_value /- def missing doc string -/ | |
| #print rbmap.find /- def missing doc string -/ | |
| #print rbmap.contains /- def missing doc string -/ | |
| #print rbmap.from_list /- def missing doc string -/ | |
| #print rbmap_of /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/rbtree/basic.lean | |
| #print rbnode /- constant missing doc string -/ | |
| #print rbnode.color /- constant missing doc string -/ | |
| #print rbnode.depth /- def missing doc string -/ | |
| #print rbnode.min /- def missing doc string -/ | |
| #print rbnode.max /- def missing doc string -/ | |
| #print rbnode.fold /- def missing doc string -/ | |
| #print rbnode.rev_fold /- def missing doc string -/ | |
| #print rbnode.balance1 /- def missing doc string -/ | |
| #print rbnode.balance1_node /- def missing doc string -/ | |
| #print rbnode.balance2 /- def missing doc string -/ | |
| #print rbnode.balance2_node /- def missing doc string -/ | |
| #print rbnode.get_color /- def missing doc string -/ | |
| #print rbnode.ins /- def missing doc string -/ | |
| #print rbnode.mk_insert_result /- def missing doc string -/ | |
| #print rbnode.insert /- def missing doc string -/ | |
| #print rbnode.mem /- def missing doc string -/ | |
| #print rbnode.mem_exact /- def missing doc string -/ | |
| #print rbnode.find /- def missing doc string -/ | |
| #print rbnode.well_formed /- constant missing doc string -/ | |
| #print rbtree /- def missing doc string -/ | |
| #print mk_rbtree /- def missing doc string -/ | |
| #print rbtree.mem /- def missing doc string -/ | |
| #print rbtree.mem_exact /- def missing doc string -/ | |
| #print rbtree.depth /- def missing doc string -/ | |
| #print rbtree.fold /- def missing doc string -/ | |
| #print rbtree.rev_fold /- def missing doc string -/ | |
| #print rbtree.empty /- def missing doc string -/ | |
| #print rbtree.to_list /- def missing doc string -/ | |
| #print rbtree.min /- def missing doc string -/ | |
| #print rbtree.max /- def missing doc string -/ | |
| #print rbtree.insert /- def missing doc string -/ | |
| #print rbtree.find /- def missing doc string -/ | |
| #print rbtree.contains /- def missing doc string -/ | |
| #print rbtree.from_list /- def missing doc string -/ | |
| #print rbtree_of /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/rbtree/default.lean | |
| #print rbtree.default_lt /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/repr.lean | |
| #print list.repr_aux /- def missing doc string -/ | |
| #print list.repr /- def missing doc string -/ | |
| #print nat.digit_char /- def missing doc string -/ | |
| #print nat.digit_succ /- def missing doc string -/ | |
| #print nat.to_digits /- def missing doc string -/ | |
| #print nat.repr /- def missing doc string -/ | |
| #print hex_digit_repr /- def missing doc string -/ | |
| #print char_to_hex /- def missing doc string -/ | |
| #print char.quote_core /- def missing doc string -/ | |
| #print string.quote_aux /- def missing doc string -/ | |
| #print string.quote /- def missing doc string -/ | |
| #print char.repr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/set.lean | |
| #print set /- def missing doc string -/ | |
| #print set_of /- def missing doc string -/ | |
| #print set.mem /- def missing doc string -/ | |
| #print set.subset /- def missing doc string -/ | |
| #print set.sep /- def missing doc string -/ | |
| #print set.univ /- def missing doc string -/ | |
| #print set.insert /- def missing doc string -/ | |
| #print set.union /- def missing doc string -/ | |
| #print set.inter /- def missing doc string -/ | |
| #print set.compl /- def missing doc string -/ | |
| #print set.diff /- def missing doc string -/ | |
| #print set.powerset /- def missing doc string -/ | |
| #print set.sUnion /- def missing doc string -/ | |
| #print set.image /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/setoid.lean | |
| #print setoid /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/sigma/lex.lean | |
| #print psigma.lex /- constant missing doc string -/ | |
| #print psigma.lex_accessible /- def missing doc string -/ | |
| #print psigma.lex_wf /- def missing doc string -/ | |
| #print psigma.lex_ndep /- def missing doc string -/ | |
| #print psigma.lex_ndep_wf /- def missing doc string -/ | |
| #print psigma.rev_lex /- constant missing doc string -/ | |
| #print psigma.rev_lex_accessible /- def missing doc string -/ | |
| #print psigma.rev_lex_wf /- def missing doc string -/ | |
| #print psigma.skip_left /- def missing doc string -/ | |
| #print psigma.skip_left_wf /- def missing doc string -/ | |
| #print psigma.mk_skip_left /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/string/basic.lean | |
| #print string_imp /- constant missing doc string -/ | |
| #print string /- def missing doc string -/ | |
| #print list.as_string /- def missing doc string -/ | |
| #print string.empty /- def missing doc string -/ | |
| #print string.length /- def missing doc string -/ | |
| #print string.push /- def missing doc string -/ | |
| #print string.append /- def missing doc string -/ | |
| #print string.to_list /- def missing doc string -/ | |
| #print string.fold /- def missing doc string -/ | |
| #print string.iterator_imp /- constant missing doc string -/ | |
| #print string.iterator /- def missing doc string -/ | |
| #print string.mk_iterator /- def missing doc string -/ | |
| #print string.iterator.curr /- def missing doc string -/ | |
| #print string.iterator.set_curr /- def missing doc string -/ | |
| #print string.iterator.next /- def missing doc string -/ | |
| #print string.iterator.prev /- def missing doc string -/ | |
| #print string.iterator.has_next /- def missing doc string -/ | |
| #print string.iterator.has_prev /- def missing doc string -/ | |
| #print string.iterator.insert /- def missing doc string -/ | |
| #print string.iterator.remove /- def missing doc string -/ | |
| #print string.iterator.to_string /- def missing doc string -/ | |
| #print string.iterator.to_end /- def missing doc string -/ | |
| #print string.iterator.next_to_string /- def missing doc string -/ | |
| #print string.iterator.prev_to_string /- def missing doc string -/ | |
| #print string.iterator.extract_core /- def missing doc string -/ | |
| #print string.iterator.extract /- def missing doc string -/ | |
| #print string.str /- def missing doc string -/ | |
| #print string.is_empty /- def missing doc string -/ | |
| #print string.front /- def missing doc string -/ | |
| #print string.back /- def missing doc string -/ | |
| #print string.join /- def missing doc string -/ | |
| #print string.singleton /- def missing doc string -/ | |
| #print string.intercalate /- def missing doc string -/ | |
| #print string.iterator.nextn /- def missing doc string -/ | |
| #print string.iterator.prevn /- def missing doc string -/ | |
| #print string.pop_back /- def missing doc string -/ | |
| #print string.popn_back /- def missing doc string -/ | |
| #print string.backn /- def missing doc string -/ | |
| #print char.to_string /- def missing doc string -/ | |
| #print string.to_nat /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/string/ops.lean | |
| #print string.split /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/subtype/basic.lean | |
| #print subtype.exists_of_subtype /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/to_string.lean | |
| #print to_string /- def missing doc string -/ | |
| #print list.to_string_aux /- def missing doc string -/ | |
| #print list.to_string /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/unsigned/basic.lean | |
| #print unsigned_sz /- def missing doc string -/ | |
| #print unsigned /- def missing doc string -/ | |
| #print unsigned.of_nat' /- def missing doc string -/ | |
| #print unsigned.to_nat /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/unsigned/ops.lean | |
| #print unsigned.of_nat /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/default.lean | |
| #print debugger.attr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/function.lean | |
| #print function.comp_right /- def missing doc string -/ | |
| #print function.comp_left /- def missing doc string -/ | |
| #print function.combine /- def missing doc string -/ | |
| #print function.swap /- def missing doc string -/ | |
| #print function.app /- def missing doc string -/ | |
| #print function.right_inverse.id /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/funext.lean | |
| #print function.equiv /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print id /- def missing doc string -/ | |
| #print flip /- def missing doc string -/ | |
| #print implies /- def missing doc string -/ | |
| #print trivial /- def missing doc string -/ | |
| #print non_contradictory /- def missing doc string -/ | |
| #print false.elim /- def missing doc string -/ | |
| #print eq.mp /- def missing doc string -/ | |
| #print eq.mpr /- def missing doc string -/ | |
| #print cast /- def missing doc string -/ | |
| #print ne /- def missing doc string -/ | |
| #print type_eq_of_heq /- def missing doc string -/ | |
| #print and.symm /- def missing doc string -/ | |
| #print not_not_em /- def missing doc string -/ | |
| #print or.symm /- def missing doc string -/ | |
| #print xor /- def missing doc string -/ | |
| #print iff /- constant missing doc string -/ | |
| #print not_not_not_iff /- def missing doc string -/ | |
| #print not_true_iff /- def missing doc string -/ | |
| #print and_implies /- def missing doc string -/ | |
| #print or.resolve_left /- def missing doc string -/ | |
| #print or.neg_resolve_left /- def missing doc string -/ | |
| #print or.resolve_right /- def missing doc string -/ | |
| #print or.neg_resolve_right /- def missing doc string -/ | |
| #print Exists /- constant missing doc string -/ | |
| #print exists.intro /- def missing doc string -/ | |
| #print exists_unique /- def missing doc string -/ | |
| #print decidable.to_bool /- def missing doc string -/ | |
| #print dite /- def missing doc string -/ | |
| #print ite /- def missing doc string -/ | |
| #print decidable.rec_on_true /- def missing doc string -/ | |
| #print decidable.rec_on_false /- def missing doc string -/ | |
| #print decidable.by_cases /- def missing doc string -/ | |
| #print decidable_of_decidable_of_iff /- def missing doc string -/ | |
| #print decidable_of_decidable_of_eq /- def missing doc string -/ | |
| #print or.by_cases /- def missing doc string -/ | |
| #print is_dec_eq /- def missing doc string -/ | |
| #print is_dec_refl /- def missing doc string -/ | |
| #print decidable_eq_of_bool_pred /- def missing doc string -/ | |
| #print inhabited /- constant missing doc string -/ | |
| #print arbitrary /- def missing doc string -/ | |
| #print nonempty /- constant missing doc string -/ | |
| #print nonempty.elim /- def missing doc string -/ | |
| #print subsingleton /- constant missing doc string -/ | |
| #print subsingleton.elim /- def missing doc string -/ | |
| #print subsingleton.helim /- def missing doc string -/ | |
| #print as_true /- def missing doc string -/ | |
| #print as_false /- def missing doc string -/ | |
| #print of_as_true /- def missing doc string -/ | |
| #print reflexive /- def missing doc string -/ | |
| #print symmetric /- def missing doc string -/ | |
| #print transitive /- def missing doc string -/ | |
| #print equivalence /- def missing doc string -/ | |
| #print total /- def missing doc string -/ | |
| #print mk_equivalence /- def missing doc string -/ | |
| #print irreflexive /- def missing doc string -/ | |
| #print anti_symmetric /- def missing doc string -/ | |
| #print empty_relation /- def missing doc string -/ | |
| #print subrelation /- def missing doc string -/ | |
| #print inv_image /- def missing doc string -/ | |
| #print tc /- constant missing doc string -/ | |
| #print commutative /- def missing doc string -/ | |
| #print associative /- def missing doc string -/ | |
| #print left_identity /- def missing doc string -/ | |
| #print right_identity /- def missing doc string -/ | |
| #print right_inverse /- def missing doc string -/ | |
| #print left_cancelative /- def missing doc string -/ | |
| #print right_cancelative /- def missing doc string -/ | |
| #print left_distributive /- def missing doc string -/ | |
| #print right_distributive /- def missing doc string -/ | |
| #print right_commutative /- def missing doc string -/ | |
| #print left_commutative /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/ac_tactics.lean | |
| #print tactic.flat_assoc /- constant missing doc string -/ | |
| #print tactic.perm_ac /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/async_tactic.lean | |
| #print tactic.run_async /- def missing doc string -/ | |
| #print tactic.prove_goal_async /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/attribute.lean | |
| #print user_attribute.dflt_parser /- def missing doc string -/ | |
| #print user_attribute.parse_reflect /- def missing doc string -/ | |
| #print user_attribute.get_param_untyped /- constant missing doc string -/ | |
| #print user_attribute.set_untyped /- constant missing doc string -/ | |
| #print user_attribute.set /- def missing doc string -/ | |
| #print get_attribute_cache_dyn /- def missing doc string -/ | |
| #print mk_name_set_attr /- def missing doc string -/ | |
| #print get_name_set_for_attr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/backward.lean | |
| #print tactic.back_lemmas /- constant missing doc string -/ | |
| #print tactic.mk_back_lemmas_core /- constant missing doc string -/ | |
| #print tactic.back_lemmas_insert_core /- constant missing doc string -/ | |
| #print tactic.back_lemmas_find /- constant missing doc string -/ | |
| #print tactic.mk_back_lemmas /- def missing doc string -/ | |
| #print tactic.back_lemmas_insert /- def missing doc string -/ | |
| #print tactic.backward_chaining_core /- constant missing doc string -/ | |
| #print tactic.back_lemmas_add_extra /- def missing doc string -/ | |
| #print tactic.back_chaining_core /- def missing doc string -/ | |
| #print tactic.back_chaining /- def missing doc string -/ | |
| #print tactic.back_chaining_using /- def missing doc string -/ | |
| #print tactic.back_chaining_using_hs /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/case_tag.lean | |
| #print tactic.interactive.case_tag.to_format /- def missing doc string -/ | |
| #print tactic.interactive.case_tag.repr /- def missing doc string -/ | |
| #print tactic.interactive.case_tag.to_string /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/comp_value_tactics.lean | |
| #print mk_nat_val_ne_proof /- constant missing doc string -/ | |
| #print mk_nat_val_lt_proof /- constant missing doc string -/ | |
| #print mk_nat_val_le_proof /- constant missing doc string -/ | |
| #print mk_fin_val_ne_proof /- constant missing doc string -/ | |
| #print mk_char_val_ne_proof /- constant missing doc string -/ | |
| #print mk_string_val_ne_proof /- constant missing doc string -/ | |
| #print mk_int_val_ne_proof /- constant missing doc string -/ | |
| #print tactic.comp_val /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/congr_lemma.lean | |
| #print congr_arg_kind.to_string /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/congr_tactic.lean | |
| #print tactic.apply_congr_core /- def missing doc string -/ | |
| #print tactic.apply_eq_congr_core /- def missing doc string -/ | |
| #print tactic.apply_heq_congr_core /- def missing doc string -/ | |
| #print tactic.congr_core /- def missing doc string -/ | |
| #print tactic.congr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/constructor_tactic.lean | |
| #print tactic.get_constructors_for /- def missing doc string -/ | |
| #print tactic.constructor /- def missing doc string -/ | |
| #print tactic.econstructor /- def missing doc string -/ | |
| #print tactic.fconstructor /- def missing doc string -/ | |
| #print tactic.left /- def missing doc string -/ | |
| #print tactic.right /- def missing doc string -/ | |
| #print tactic.constructor_idx /- def missing doc string -/ | |
| #print tactic.split /- def missing doc string -/ | |
| #print tactic.existsi /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/contradiction_tactic.lean | |
| #print tactic.contradiction /- def missing doc string -/ | |
| #print tactic.exfalso /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/converter/conv.lean | |
| #print conv.lhs /- def missing doc string -/ | |
| #print conv.rhs /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/converter/interactive.lean | |
| #print conv.save_info /- def missing doc string -/ | |
| #print conv.step /- def missing doc string -/ | |
| #print conv.istep /- def missing doc string -/ | |
| #print conv.execute /- def missing doc string -/ | |
| #print conv.solve1 /- def missing doc string -/ | |
| #print conv.interactive.itactic /- def missing doc string -/ | |
| #print conv.interactive.skip /- def missing doc string -/ | |
| #print conv.interactive.whnf /- def missing doc string -/ | |
| #print conv.interactive.dsimp /- def missing doc string -/ | |
| #print conv.interactive.trace_lhs /- def missing doc string -/ | |
| #print conv.interactive.change /- def missing doc string -/ | |
| #print conv.interactive.congr /- def missing doc string -/ | |
| #print conv.interactive.funext /- def missing doc string -/ | |
| #print conv.interactive.to_lhs /- def missing doc string -/ | |
| #print conv.interactive.to_rhs /- def missing doc string -/ | |
| #print conv.interactive.done /- def missing doc string -/ | |
| #print conv.interactive.find /- def missing doc string -/ | |
| #print conv.interactive.for /- def missing doc string -/ | |
| #print conv.interactive.simp /- def missing doc string -/ | |
| #print conv.interactive.guard_lhs /- def missing doc string -/ | |
| #print conv.interactive.rewrite /- def missing doc string -/ | |
| #print conv.interactive.rw /- def missing doc string -/ | |
| #print tactic.interactive.conv /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/declaration.lean | |
| #print mk_definition /- def missing doc string -/ | |
| #print declaration.to_name /- def missing doc string -/ | |
| #print declaration.univ_params /- def missing doc string -/ | |
| #print declaration.type /- def missing doc string -/ | |
| #print declaration.value /- def missing doc string -/ | |
| #print declaration.value_task /- def missing doc string -/ | |
| #print declaration.is_trusted /- def missing doc string -/ | |
| #print declaration.update_type /- def missing doc string -/ | |
| #print declaration.update_name /- def missing doc string -/ | |
| #print declaration.update_value /- def missing doc string -/ | |
| #print declaration.update_value_task /- def missing doc string -/ | |
| #print declaration.map_value /- def missing doc string -/ | |
| #print declaration.to_definition /- def missing doc string -/ | |
| #print declaration.is_definition /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/derive.lean | |
| #print derive_handler_attr /- def missing doc string -/ | |
| #print derive_attr /- def missing doc string -/ | |
| #print has_reflect_derive_handler /- def missing doc string -/ | |
| #print has_sizeof_derive_handler /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/environment.lean | |
| #print environment.contains /- def missing doc string -/ | |
| #print environment.add_defn_eqns /- constant missing doc string -/ | |
| #print environment.unfold_untrusted_macros /- constant missing doc string -/ | |
| #print environment.unfold_all_macros /- constant missing doc string -/ | |
| #print environment.is_constructor_app /- def missing doc string -/ | |
| #print environment.is_refl_app /- def missing doc string -/ | |
| #print environment.is_definition /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/exceptional.lean | |
| #print exceptional.to_string /- def missing doc string -/ | |
| #print exceptional.to_bool /- def missing doc string -/ | |
| #print exceptional.to_option /- def missing doc string -/ | |
| #print exceptional.bind /- def missing doc string -/ | |
| #print exceptional.return /- def missing doc string -/ | |
| #print exceptional.fail /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/expr.lean | |
| #print expr.mk_var /- def missing doc string -/ | |
| #print expr.to_string /- constant missing doc string -/ | |
| #print reflected.to_expr /- def missing doc string -/ | |
| #print reflected.subst /- def missing doc string -/ | |
| #print reflect /- def missing doc string -/ | |
| #print expr.expr.lt_prop /- def missing doc string -/ | |
| #print expr.mk_true /- def missing doc string -/ | |
| #print expr.mk_false /- def missing doc string -/ | |
| #print expr.instantiate_locals /- def missing doc string -/ | |
| #print expr.is_var /- def missing doc string -/ | |
| #print expr.app_of_list /- def missing doc string -/ | |
| #print expr.is_app /- def missing doc string -/ | |
| #print expr.app_fn /- def missing doc string -/ | |
| #print expr.app_arg /- def missing doc string -/ | |
| #print expr.get_app_fn /- def missing doc string -/ | |
| #print expr.get_app_num_args /- def missing doc string -/ | |
| #print expr.get_app_args_aux /- def missing doc string -/ | |
| #print expr.get_app_args /- def missing doc string -/ | |
| #print expr.mk_app /- def missing doc string -/ | |
| #print expr.mk_binding /- def missing doc string -/ | |
| #print expr.ith_arg_aux /- def missing doc string -/ | |
| #print expr.ith_arg /- def missing doc string -/ | |
| #print expr.const_name /- def missing doc string -/ | |
| #print expr.is_constant /- def missing doc string -/ | |
| #print expr.is_local_constant /- def missing doc string -/ | |
| #print expr.local_uniq_name /- def missing doc string -/ | |
| #print expr.local_pp_name /- def missing doc string -/ | |
| #print expr.local_type /- def missing doc string -/ | |
| #print expr.is_aux_decl /- def missing doc string -/ | |
| #print expr.is_constant_of /- def missing doc string -/ | |
| #print expr.is_app_of /- def missing doc string -/ | |
| #print expr.is_false /- def missing doc string -/ | |
| #print expr.is_not /- def missing doc string -/ | |
| #print expr.is_and /- def missing doc string -/ | |
| #print expr.is_or /- def missing doc string -/ | |
| #print expr.is_iff /- def missing doc string -/ | |
| #print expr.is_eq /- def missing doc string -/ | |
| #print expr.is_ne /- def missing doc string -/ | |
| #print expr.is_bin_arith_app /- def missing doc string -/ | |
| #print expr.is_lt /- def missing doc string -/ | |
| #print expr.is_gt /- def missing doc string -/ | |
| #print expr.is_le /- def missing doc string -/ | |
| #print expr.is_ge /- def missing doc string -/ | |
| #print expr.is_heq /- def missing doc string -/ | |
| #print expr.is_lambda /- def missing doc string -/ | |
| #print expr.is_pi /- def missing doc string -/ | |
| #print expr.is_arrow /- def missing doc string -/ | |
| #print expr.is_let /- def missing doc string -/ | |
| #print expr.binding_name /- def missing doc string -/ | |
| #print expr.binding_info /- def missing doc string -/ | |
| #print expr.binding_domain /- def missing doc string -/ | |
| #print expr.binding_body /- def missing doc string -/ | |
| #print expr.is_macro /- def missing doc string -/ | |
| #print expr.is_numeral /- def missing doc string -/ | |
| #print expr.imp /- def missing doc string -/ | |
| #print expr.extract_opt_auto_param /- def missing doc string -/ | |
| #print expr.to_raw_fmt /- def missing doc string -/ | |
| #print expr_map.mk /- def missing doc string -/ | |
| #print mk_expr_map /- def missing doc string -/ | |
| #print expr_set /- def missing doc string -/ | |
| #print mk_expr_set /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/float.lean | |
| #print native.float /- constant missing doc string -/ | |
| #print native.float.is_finite /- constant missing doc string -/ | |
| #print native.float.add /- constant missing doc string -/ | |
| #print native.float.sub /- constant missing doc string -/ | |
| #print native.float.neg /- constant missing doc string -/ | |
| #print native.float.mul /- constant missing doc string -/ | |
| #print native.float.div /- constant missing doc string -/ | |
| #print native.float.max /- constant missing doc string -/ | |
| #print native.float.min /- constant missing doc string -/ | |
| #print native.float.pow /- constant missing doc string -/ | |
| #print native.float.log2 /- constant missing doc string -/ | |
| #print native.float.log10 /- constant missing doc string -/ | |
| #print native.float.pi /- constant missing doc string -/ | |
| #print native.float.sin /- constant missing doc string -/ | |
| #print native.float.cos /- constant missing doc string -/ | |
| #print native.float.tan /- constant missing doc string -/ | |
| #print native.float.asin /- constant missing doc string -/ | |
| #print native.float.acos /- constant missing doc string -/ | |
| #print native.float.atan /- constant missing doc string -/ | |
| #print native.float.sinh /- constant missing doc string -/ | |
| #print native.float.cosh /- constant missing doc string -/ | |
| #print native.float.tanh /- constant missing doc string -/ | |
| #print native.float.asinh /- constant missing doc string -/ | |
| #print native.float.acosh /- constant missing doc string -/ | |
| #print native.float.atanh /- constant missing doc string -/ | |
| #print native.float.abs /- constant missing doc string -/ | |
| #print native.float.lt /- constant missing doc string -/ | |
| #print native.float.le /- constant missing doc string -/ | |
| #print native.float.of_nat /- constant missing doc string -/ | |
| #print native.float.of_int /- constant missing doc string -/ | |
| #print native.float.zero /- def missing doc string -/ | |
| #print native.float.one /- def missing doc string -/ | |
| #print native.float.to_repr /- constant missing doc string -/ | |
| #print native.float.of_string /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/format.lean | |
| #print format.color /- constant missing doc string -/ | |
| #print format.of_string /- constant missing doc string -/ | |
| #print format.of_nat /- constant missing doc string -/ | |
| #print format.to_string /- constant missing doc string -/ | |
| #print format.of_options /- constant missing doc string -/ | |
| #print format.is_nil /- constant missing doc string -/ | |
| #print to_fmt /- def missing doc string -/ | |
| #print format.indent /- def missing doc string -/ | |
| #print format.when /- def missing doc string -/ | |
| #print format.join /- def missing doc string -/ | |
| #print list.to_format /- def missing doc string -/ | |
| #print format.bracket /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/fun_info.lean | |
| #print param_info /- constant missing doc string -/ | |
| #print param_info.to_format /- def missing doc string -/ | |
| #print fun_info /- constant missing doc string -/ | |
| #print fun_info_to_format /- def missing doc string -/ | |
| #print subsingleton_info_to_format /- def missing doc string -/ | |
| #print tactic.get_subsingleton_info /- constant missing doc string -/ | |
| #print tactic.get_spec_prefix_size /- constant missing doc string -/ | |
| #print tactic.fold_explicit_args_aux /- def missing doc string -/ | |
| #print tactic.fold_explicit_args /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/has_reflect.lean | |
| #print reflected_value /- constant missing doc string -/ | |
| #print reflected_value.expr /- def missing doc string -/ | |
| #print reflected_value.subst /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/hole_command.lean | |
| #print infer_type_cmd /- def missing doc string -/ | |
| #print show_goal_cmd /- def missing doc string -/ | |
| #print use_cmd /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/injection_tactic.lean | |
| #print tactic.injection_with /- def missing doc string -/ | |
| #print tactic.injection /- def missing doc string -/ | |
| #print tactic.injections_with /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/interaction_monad.lean | |
| #print interaction_monad.result /- constant missing doc string -/ | |
| #print interaction_monad.result_to_string /- def missing doc string -/ | |
| #print interaction_monad.result.clamp_pos /- def missing doc string -/ | |
| #print interaction_monad /- def missing doc string -/ | |
| #print interaction_monad_fmap /- def missing doc string -/ | |
| #print interaction_monad_bind /- def missing doc string -/ | |
| #print interaction_monad_return /- def missing doc string -/ | |
| #print interaction_monad_orelse /- def missing doc string -/ | |
| #print interaction_monad_seq /- def missing doc string -/ | |
| #print interaction_monad.mk_exception /- def missing doc string -/ | |
| #print interaction_monad.fail /- def missing doc string -/ | |
| #print interaction_monad.silent_fail /- def missing doc string -/ | |
| #print interaction_monad.failed /- def missing doc string -/ | |
| #print interaction_monad.orelse' /- def missing doc string -/ | |
| #print interaction_monad.bracket /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/interactive.lean | |
| #print tactic.i_to_expr /- def missing doc string -/ | |
| #print tactic.i_to_expr_no_subgoals /- def missing doc string -/ | |
| #print tactic.i_to_expr_strict /- def missing doc string -/ | |
| #print tactic.i_to_expr_for_apply /- def missing doc string -/ | |
| #print tactic.interactive.propagate_tags /- def missing doc string -/ | |
| #print tactic.interactive.concat_tags /- def missing doc string -/ | |
| #print tactic.interactive.to_expr' /- def missing doc string -/ | |
| #print tactic.interactive.rw_rule /- constant missing doc string -/ | |
| #print tactic.interactive.get_rule_eqn_lemmas /- def missing doc string -/ | |
| #print tactic.interactive.rw_rule_p /- def missing doc string -/ | |
| #print tactic.interactive.rw_rules_t /- constant missing doc string -/ | |
| #print tactic.interactive.rw_rules /- def missing doc string -/ | |
| #print tactic.interactive.cases_arg_p /- def missing doc string -/ | |
| #print tactic.interactive.cases_core /- def missing doc string -/ | |
| #print tactic.interactive.constructor_matching /- def missing doc string -/ | |
| #print tactic.simp_config_ext /- constant missing doc string -/ | |
| #print tactic.simp_arg_type /- constant missing doc string -/ | |
| #print tactic.simp_arg /- def missing doc string -/ | |
| #print tactic.simp_arg_list /- def missing doc string -/ | |
| #print tactic.mk_simp_set_core /- def missing doc string -/ | |
| #print tactic.mk_simp_set /- def missing doc string -/ | |
| #print tactic.interactive.simp_core_aux /- def missing doc string -/ | |
| #print tactic.interactive.simp_core /- def missing doc string -/ | |
| #print tactic.ids_to_simp_arg_list /- def missing doc string -/ | |
| #print tactic.unfold_config /- constant missing doc string -/ | |
| #print tactic.interactive.guard_expr_eq /- def missing doc string -/ | |
| #print tactic.interactive.congr /- def missing doc string -/ | |
| #print has_dup /- def missing doc string -/ | |
| #print tactic.apply_inj_lemma /- def missing doc string -/ | |
| #print tactic.mk_inj_eq /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/interactive_base.lean | |
| #print interactive.loc.include_goal /- def missing doc string -/ | |
| #print interactive.loc.get_locals /- def missing doc string -/ | |
| #print interactive.loc.apply /- def missing doc string -/ | |
| #print interactive.loc.try_apply /- def missing doc string -/ | |
| #print interactive.types.brackets /- def missing doc string -/ | |
| #print interactive.types.list_of /- def missing doc string -/ | |
| #print interactive.types.using_ident /- def missing doc string -/ | |
| #print interactive.types.with_ident_list /- def missing doc string -/ | |
| #print interactive.types.without_ident_list /- def missing doc string -/ | |
| #print interactive.types.location /- def missing doc string -/ | |
| #print interactive.types.pexpr_list /- def missing doc string -/ | |
| #print interactive.types.opt_pexpr_list /- def missing doc string -/ | |
| #print interactive.types.pexpr_list_or_texpr /- def missing doc string -/ | |
| #print interactive.types.only_flag /- def missing doc string -/ | |
| #print interactive.param_desc /- def missing doc string -/ | |
| #print interactive.parse_binders_core /- constant missing doc string -/ | |
| #print interactive.parse_binders /- def missing doc string -/ | |
| #print interactive.decl_attributes /- constant missing doc string -/ | |
| #print interactive.decl_attributes.apply /- constant missing doc string -/ | |
| #print interactive.decl_modifiers /- constant missing doc string -/ | |
| #print interactive.decl_meta_info /- constant missing doc string -/ | |
| #print interactive.single_inductive_decl /- constant missing doc string -/ | |
| #print interactive.single_inductive_decl.name /- def missing doc string -/ | |
| #print interactive.inductive_decl /- constant missing doc string -/ | |
| #print format_macro /- def missing doc string -/ | |
| #print sformat_macro /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/lean/parser.lean | |
| #print lean.parser_state /- constant missing doc string -/ | |
| #print lean.parser_state.env /- constant missing doc string -/ | |
| #print lean.parser_state.options /- constant missing doc string -/ | |
| #print lean.parser_state.cur_pos /- constant missing doc string -/ | |
| #print lean.parser /- def missing doc string -/ | |
| #print lean.parser_result /- def missing doc string -/ | |
| #print lean.parser.val /- def missing doc string -/ | |
| #print lean.parser.reflectable /- constant missing doc string -/ | |
| #print lean.parser.reflectable.expr /- def missing doc string -/ | |
| #print lean.parser.reflectable.to_parser /- def missing doc string -/ | |
| #print lean.parser.get_env /- def missing doc string -/ | |
| #print lean.parser.set_env /- constant missing doc string -/ | |
| #print lean.parser.add_local_level /- constant missing doc string -/ | |
| #print lean.parser.list_include_var_names /- constant missing doc string -/ | |
| #print lean.parser.list_available_include_vars /- constant missing doc string -/ | |
| #print lean.parser.include_var /- constant missing doc string -/ | |
| #print lean.parser.omit_var /- constant missing doc string -/ | |
| #print lean.parser.push_local_scope /- constant missing doc string -/ | |
| #print lean.parser.pop_local_scope /- constant missing doc string -/ | |
| #print lean.parser.itactic_reflected /- constant missing doc string -/ | |
| #print lean.parser.parser_orelse /- def missing doc string -/ | |
| #print lean.parser.many /- def missing doc string -/ | |
| #print lean.parser.sep_by /- def missing doc string -/ | |
| #print lean.parser.of_tactic /- constant missing doc string -/ | |
| #print lean.parser.reflect /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/level.lean | |
| #print level.lt /- constant missing doc string -/ | |
| #print level.lex_lt /- constant missing doc string -/ | |
| #print level.fold /- constant missing doc string -/ | |
| #print level.to_format /- constant missing doc string -/ | |
| #print level.to_string /- constant missing doc string -/ | |
| #print level.of_nat /- def missing doc string -/ | |
| #print level.has_param /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/local_context.lean | |
| #print local_decl /- constant missing doc string -/ | |
| #print local_context.get_local_decl /- constant missing doc string -/ | |
| #print local_context.get_local /- constant missing doc string -/ | |
| #print local_context.is_subset /- constant missing doc string -/ | |
| #print local_context.fold /- constant missing doc string -/ | |
| #print local_context.to_list /- def missing doc string -/ | |
| #print local_context.to_format /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/mk_dec_eq_instance.lean | |
| #print tactic.mk_dec_eq_instance_core /- def missing doc string -/ | |
| #print tactic.mk_dec_eq_instance /- def missing doc string -/ | |
| #print tactic.decidable_eq_derive_handler /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/mk_has_sizeof_instance.lean | |
| #print tactic.mk_has_sizeof_instance_core /- def missing doc string -/ | |
| #print tactic.mk_has_sizeof_instance /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/mk_inhabited_instance.lean | |
| #print tactic.mk_inhabited_instance /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/name.lean | |
| #print mk_str_name /- def missing doc string -/ | |
| #print mk_num_name /- def missing doc string -/ | |
| #print mk_simple_name /- def missing doc string -/ | |
| #print name.get_prefix /- def missing doc string -/ | |
| #print name.update_prefix /- def missing doc string -/ | |
| #print name.to_string_with_sep /- def missing doc string -/ | |
| #print name.components /- def missing doc string -/ | |
| #print name.to_string /- def missing doc string -/ | |
| #print name.repr /- def missing doc string -/ | |
| #print name.cmp /- constant missing doc string -/ | |
| #print name.lex_cmp /- constant missing doc string -/ | |
| #print name.append /- constant missing doc string -/ | |
| #print name.is_internal /- constant missing doc string -/ | |
| #print name.lt /- def missing doc string -/ | |
| #print name.is_prefix_of /- def missing doc string -/ | |
| #print name.is_suffix_of /- def missing doc string -/ | |
| #print name.replace_prefix /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/occurrences.lean | |
| #print occurrences.contains /- def missing doc string -/ | |
| #print occurrences_repr /- def missing doc string -/ | |
| #print occurrences_to_format /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/options.lean | |
| #print options /- constant missing doc string -/ | |
| #print options.size /- constant missing doc string -/ | |
| #print options.mk /- constant missing doc string -/ | |
| #print options.contains /- constant missing doc string -/ | |
| #print options.set_bool /- constant missing doc string -/ | |
| #print options.set_nat /- constant missing doc string -/ | |
| #print options.set_string /- constant missing doc string -/ | |
| #print options.get_bool /- constant missing doc string -/ | |
| #print options.get_nat /- constant missing doc string -/ | |
| #print options.get_string /- constant missing doc string -/ | |
| #print options.join /- constant missing doc string -/ | |
| #print options.fold /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/pexpr.lean | |
| #print pexpr.of_expr /- constant missing doc string -/ | |
| #print pexpr.is_placeholder /- constant missing doc string -/ | |
| #print pexpr.mk_placeholder /- constant missing doc string -/ | |
| #print pexpr.mk_field_macro /- constant missing doc string -/ | |
| #print pexpr.mk_explicit /- constant missing doc string -/ | |
| #print pexpr.get_structure_instance_info /- constant missing doc string -/ | |
| #print has_to_pexpr /- constant missing doc string -/ | |
| #print to_pexpr /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/rb_map.lean | |
| #print native.rb_map /- constant missing doc string -/ | |
| #print native.rb_map.mk_core /- constant missing doc string -/ | |
| #print native.rb_map.size /- constant missing doc string -/ | |
| #print native.rb_map.empty /- constant missing doc string -/ | |
| #print native.rb_map.insert /- constant missing doc string -/ | |
| #print native.rb_map.erase /- constant missing doc string -/ | |
| #print native.rb_map.contains /- constant missing doc string -/ | |
| #print native.rb_map.find /- constant missing doc string -/ | |
| #print native.rb_map.min /- constant missing doc string -/ | |
| #print native.rb_map.max /- constant missing doc string -/ | |
| #print native.rb_map.fold /- constant missing doc string -/ | |
| #print native.rb_map.mk /- def missing doc string -/ | |
| #print native.rb_map.keys /- def missing doc string -/ | |
| #print native.rb_map.values /- def missing doc string -/ | |
| #print native.rb_map.to_list /- def missing doc string -/ | |
| #print native.rb_map.mfold /- def missing doc string -/ | |
| #print native.rb_map.of_list /- def missing doc string -/ | |
| #print native.rb_map.set_of_list /- def missing doc string -/ | |
| #print native.rb_map.map /- def missing doc string -/ | |
| #print native.rb_map.for /- def missing doc string -/ | |
| #print native.rb_map.filter /- def missing doc string -/ | |
| #print native.mk_rb_map /- def missing doc string -/ | |
| #print native.nat_map /- def missing doc string -/ | |
| #print native.nat_map.mk /- def missing doc string -/ | |
| #print native.mk_nat_map /- def missing doc string -/ | |
| #print native.rb_lmap.mk /- def missing doc string -/ | |
| #print native.rb_lmap.insert /- def missing doc string -/ | |
| #print native.rb_lmap.erase /- def missing doc string -/ | |
| #print native.rb_lmap.contains /- def missing doc string -/ | |
| #print native.rb_lmap.find /- def missing doc string -/ | |
| #print native.rb_set /- def missing doc string -/ | |
| #print native.mk_rb_set /- def missing doc string -/ | |
| #print native.rb_set.insert /- def missing doc string -/ | |
| #print native.rb_set.erase /- def missing doc string -/ | |
| #print native.rb_set.contains /- def missing doc string -/ | |
| #print native.rb_set.size /- def missing doc string -/ | |
| #print native.rb_set.empty /- def missing doc string -/ | |
| #print native.rb_set.fold /- def missing doc string -/ | |
| #print native.rb_set.mfold /- def missing doc string -/ | |
| #print native.rb_set.to_list /- def missing doc string -/ | |
| #print name_map /- def missing doc string -/ | |
| #print name_map.mk /- def missing doc string -/ | |
| #print mk_name_map /- def missing doc string -/ | |
| #print mk_name_set /- constant missing doc string -/ | |
| #print name_set.insert /- constant missing doc string -/ | |
| #print name_set.erase /- constant missing doc string -/ | |
| #print name_set.contains /- constant missing doc string -/ | |
| #print name_set.size /- constant missing doc string -/ | |
| #print name_set.empty /- constant missing doc string -/ | |
| #print name_set.fold /- constant missing doc string -/ | |
| #print name_set.to_list /- def missing doc string -/ | |
| #print name_set.of_list /- def missing doc string -/ | |
| #print name_set.mfold /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/rec_util.lean | |
| #print tactic.constructor_num_fields /- def missing doc string -/ | |
| #print tactic.mk_constructor_fresh_names /- def missing doc string -/ | |
| #print tactic.mk_constructors_fresh_names /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/relation_tactics.lean | |
| #print tactic.reflexivity /- def missing doc string -/ | |
| #print tactic.symmetry /- def missing doc string -/ | |
| #print tactic.transitivity /- def missing doc string -/ | |
| #print tactic.relation_lhs_rhs /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/rewrite_tactic.lean | |
| #print tactic.rewrite /- def missing doc string -/ | |
| #print tactic.rewrite_target /- def missing doc string -/ | |
| #print tactic.rewrite_hyp /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/set_get_option_tactics.lean | |
| #print tactic.set_bool_option /- def missing doc string -/ | |
| #print tactic.set_nat_option /- def missing doc string -/ | |
| #print tactic.set_string_option /- def missing doc string -/ | |
| #print tactic.get_bool_option /- def missing doc string -/ | |
| #print tactic.get_nat_option /- def missing doc string -/ | |
| #print tactic.get_string_option /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/simp_tactic.lean | |
| #print simp.default_max_steps /- def missing doc string -/ | |
| #print simp_lemmas.rewrites /- constant missing doc string -/ | |
| #print is_valid_simp_lemma_cnst /- constant missing doc string -/ | |
| #print is_valid_simp_lemma /- constant missing doc string -/ | |
| #print simp_lemmas.pp /- constant missing doc string -/ | |
| #print tactic.dsimp_config /- constant missing doc string -/ | |
| #print tactic.dsimplify_core /- constant missing doc string -/ | |
| #print tactic.dsimplify /- def missing doc string -/ | |
| #print tactic.get_simp_lemmas_or_default /- def missing doc string -/ | |
| #print tactic.dsimp_target /- def missing doc string -/ | |
| #print tactic.dsimp_hyp /- def missing doc string -/ | |
| #print tactic.dunfold_config /- constant missing doc string -/ | |
| #print tactic.dunfold /- constant missing doc string -/ | |
| #print tactic.dunfold_target /- def missing doc string -/ | |
| #print tactic.dunfold_hyp /- def missing doc string -/ | |
| #print tactic.delta_config /- constant missing doc string -/ | |
| #print tactic.delta_target /- def missing doc string -/ | |
| #print tactic.delta_hyp /- def missing doc string -/ | |
| #print tactic.unfold_proj_config /- constant missing doc string -/ | |
| #print tactic.unfold_projs /- def missing doc string -/ | |
| #print tactic.unfold_projs_target /- def missing doc string -/ | |
| #print tactic.unfold_projs_hyp /- def missing doc string -/ | |
| #print tactic.simp_config /- constant missing doc string -/ | |
| #print tactic.simp_target /- def missing doc string -/ | |
| #print tactic.simp_hyp /- def missing doc string -/ | |
| #print tactic.collect_ctx_simps /- def missing doc string -/ | |
| #print tactic.intro1_aux /- def missing doc string -/ | |
| #print tactic.simp_intros_config /- constant missing doc string -/ | |
| #print tactic.simp_intros_aux /- def missing doc string -/ | |
| #print tactic.simp_intros /- def missing doc string -/ | |
| #print tactic.mk_eq_simp_ext /- def missing doc string -/ | |
| #print tactic.to_simp_lemmas /- def missing doc string -/ | |
| #print tactic.mk_simp_attr /- def missing doc string -/ | |
| #print tactic.join_user_simp_lemmas_core /- def missing doc string -/ | |
| #print tactic.join_user_simp_lemmas /- def missing doc string -/ | |
| #print tactic.simplify_top_down /- def missing doc string -/ | |
| #print tactic.simp_top_down /- def missing doc string -/ | |
| #print tactic.simplify_bottom_up /- def missing doc string -/ | |
| #print tactic.simp_bottom_up /- def missing doc string -/ | |
| #print tactic.non_dep_prop_hyps /- def missing doc string -/ | |
| #print tactic.simp_all_entry /- constant missing doc string -/ | |
| #print tactic.simp_all /- def missing doc string -/ | |
| #print tactic.trace_algebra_info /- constant missing doc string -/ | |
| #print simp_attr.norm /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/congruence_closure.lean | |
| #print cc_config /- constant missing doc string -/ | |
| #print cc_state.mk_core /- constant missing doc string -/ | |
| #print cc_state.next /- constant missing doc string -/ | |
| #print cc_state.roots_core /- constant missing doc string -/ | |
| #print cc_state.root /- constant missing doc string -/ | |
| #print cc_state.mt /- constant missing doc string -/ | |
| #print cc_state.gmt /- constant missing doc string -/ | |
| #print cc_state.inc_gmt /- constant missing doc string -/ | |
| #print cc_state.is_cg_root /- constant missing doc string -/ | |
| #print cc_state.pp_eqc /- constant missing doc string -/ | |
| #print cc_state.pp_core /- constant missing doc string -/ | |
| #print cc_state.internalize /- constant missing doc string -/ | |
| #print cc_state.add /- constant missing doc string -/ | |
| #print cc_state.is_eqv /- constant missing doc string -/ | |
| #print cc_state.is_not_eqv /- constant missing doc string -/ | |
| #print cc_state.eqv_proof /- constant missing doc string -/ | |
| #print cc_state.inconsistent /- constant missing doc string -/ | |
| #print cc_state.mk /- def missing doc string -/ | |
| #print cc_state.mk_using_hs /- def missing doc string -/ | |
| #print cc_state.roots /- def missing doc string -/ | |
| #print cc_state.eqc_of_core /- def missing doc string -/ | |
| #print cc_state.eqc_of /- def missing doc string -/ | |
| #print cc_state.in_singlenton_eqc /- def missing doc string -/ | |
| #print cc_state.eqc_size /- def missing doc string -/ | |
| #print cc_state.fold_eqc_core /- def missing doc string -/ | |
| #print cc_state.fold_eqc /- def missing doc string -/ | |
| #print cc_state.mfold_eqc /- def missing doc string -/ | |
| #print tactic.cc_core /- def missing doc string -/ | |
| #print tactic.cc /- def missing doc string -/ | |
| #print tactic.cc_dbg_core /- def missing doc string -/ | |
| #print tactic.cc_dbg /- def missing doc string -/ | |
| #print tactic.ac_refl /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/ematch.lean | |
| #print hinst_lemmas /- constant missing doc string -/ | |
| #print hinst_lemma.mk_from_decl_core /- constant missing doc string -/ | |
| #print hinst_lemma.pp /- constant missing doc string -/ | |
| #print hinst_lemma.id /- constant missing doc string -/ | |
| #print hinst_lemma.mk /- def missing doc string -/ | |
| #print hinst_lemma.mk_from_decl /- def missing doc string -/ | |
| #print hinst_lemmas.mk /- constant missing doc string -/ | |
| #print hinst_lemmas.add /- constant missing doc string -/ | |
| #print hinst_lemmas.fold /- constant missing doc string -/ | |
| #print hinst_lemmas.merge /- constant missing doc string -/ | |
| #print mk_hinst_singleton /- def missing doc string -/ | |
| #print hinst_lemmas.pp /- def missing doc string -/ | |
| #print to_hinst_lemmas_core /- def missing doc string -/ | |
| #print mk_hinst_lemma_attr_core /- def missing doc string -/ | |
| #print mk_hinst_lemma_attrs_core /- def missing doc string -/ | |
| #print merge_hinst_lemma_attrs /- def missing doc string -/ | |
| #print get_hinst_lemmas_for_attr /- def missing doc string -/ | |
| #print ematch_config /- constant missing doc string -/ | |
| #print ematch_state /- constant missing doc string -/ | |
| #print ematch_state.mk /- constant missing doc string -/ | |
| #print ematch_state.internalize /- constant missing doc string -/ | |
| #print tactic.ematch_core /- constant missing doc string -/ | |
| #print tactic.ematch_all_core /- constant missing doc string -/ | |
| #print tactic.ematch /- def missing doc string -/ | |
| #print tactic.ematch_all /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/interactive.lean | |
| #print smt_tactic.save_info /- def missing doc string -/ | |
| #print smt_tactic.skip /- def missing doc string -/ | |
| #print smt_tactic.solve_goals /- def missing doc string -/ | |
| #print smt_tactic.step /- def missing doc string -/ | |
| #print smt_tactic.istep /- def missing doc string -/ | |
| #print smt_tactic.execute /- def missing doc string -/ | |
| #print smt_tactic.execute_with /- def missing doc string -/ | |
| #print smt_tactic.interactive.itactic /- def missing doc string -/ | |
| #print smt_tactic.interactive.intros /- def missing doc string -/ | |
| #print smt_tactic.interactive.apply /- def missing doc string -/ | |
| #print smt_tactic.interactive.fapply /- def missing doc string -/ | |
| #print smt_tactic.interactive.apply_instance /- def missing doc string -/ | |
| #print smt_tactic.interactive.change /- def missing doc string -/ | |
| #print smt_tactic.interactive.exact /- def missing doc string -/ | |
| #print smt_tactic.interactive.from /- def missing doc string -/ | |
| #print smt_tactic.interactive.assume /- def missing doc string -/ | |
| #print smt_tactic.interactive.have /- def missing doc string -/ | |
| #print smt_tactic.interactive.let /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_fact /- def missing doc string -/ | |
| #print smt_tactic.interactive.trace_state /- def missing doc string -/ | |
| #print smt_tactic.interactive.trace /- def missing doc string -/ | |
| #print smt_tactic.interactive.destruct /- def missing doc string -/ | |
| #print smt_tactic.interactive.by_cases /- def missing doc string -/ | |
| #print smt_tactic.interactive.by_contradiction /- def missing doc string -/ | |
| #print smt_tactic.interactive.by_contra /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_lemma /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_lhs_lemma /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_eqn_lemmas_for /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_eqn_lemmas /- def missing doc string -/ | |
| #print smt_tactic.interactive.ematch_using /- def missing doc string -/ | |
| #print smt_tactic.interactive.induction /- def missing doc string -/ | |
| #print smt_tactic.interactive.dsimp /- def missing doc string -/ | |
| #print smt_tactic.interactive.rsimp /- def missing doc string -/ | |
| #print smt_tactic.interactive.add_simp_lemmas /- def missing doc string -/ | |
| #print smt_tactic.interactive.guard_expr_eq /- def missing doc string -/ | |
| #print smt_tactic.interactive.guard_target /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/rsimp.lean | |
| #print no_rsimp /- def missing doc string -/ | |
| #print rsimp_attr /- def missing doc string -/ | |
| #print rsimp.is_value_like /- def missing doc string -/ | |
| #print rsimp.repr_map /- def missing doc string -/ | |
| #print rsimp.mk_repr_map /- def missing doc string -/ | |
| #print rsimp.to_repr_map /- def missing doc string -/ | |
| #print rsimp.rsimplify /- def missing doc string -/ | |
| #print rsimp.config /- constant missing doc string -/ | |
| #print rsimp.collect_implied_eqs /- def missing doc string -/ | |
| #print rsimp.rsimplify_goal /- def missing doc string -/ | |
| #print rsimp.rsimplify_at /- def missing doc string -/ | |
| #print tactic.rsimp /- def missing doc string -/ | |
| #print tactic.rsimp_at /- def missing doc string -/ | |
| #print tactic.interactive.rsimp /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/smt_tactic.lean | |
| #print simp_attr.pre_smt /- def missing doc string -/ | |
| #print ematch /- def missing doc string -/ | |
| #print ematch_lhs /- def missing doc string -/ | |
| #print smt_config.set_classical /- def missing doc string -/ | |
| #print smt_goal /- constant missing doc string -/ | |
| #print smt_state /- def missing doc string -/ | |
| #print smt_state.mk /- constant missing doc string -/ | |
| #print smt_state.to_format /- constant missing doc string -/ | |
| #print smt_tactic /- def missing doc string -/ | |
| #print tactic_to_smt_tactic /- constant missing doc string -/ | |
| #print smt_tactic.intros /- constant missing doc string -/ | |
| #print smt_tactic.intron /- constant missing doc string -/ | |
| #print smt_tactic.intro_lst /- constant missing doc string -/ | |
| #print smt_tactic.mk_ematch_eqn_lemmas_for_core /- constant missing doc string -/ | |
| #print smt_tactic.to_cc_state /- constant missing doc string -/ | |
| #print smt_tactic.to_em_state /- constant missing doc string -/ | |
| #print smt_tactic.get_config /- constant missing doc string -/ | |
| #print smt_tactic.get_lemmas /- constant missing doc string -/ | |
| #print smt_tactic.set_lemmas /- constant missing doc string -/ | |
| #print smt_tactic.add_lemmas /- constant missing doc string -/ | |
| #print smt_tactic.add_ematch_lemma_core /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_lemma_from_decl_core /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_eqn_lemmas_for_core /- def missing doc string -/ | |
| #print smt_tactic.ematch /- def missing doc string -/ | |
| #print smt_tactic.failed /- def missing doc string -/ | |
| #print smt_tactic.fail /- def missing doc string -/ | |
| #print smt_tactic.try /- def missing doc string -/ | |
| #print smt_tactic.iterate /- def missing doc string -/ | |
| #print smt_tactic.eblast /- def missing doc string -/ | |
| #print smt_tactic.read /- def missing doc string -/ | |
| #print smt_tactic.write /- def missing doc string -/ | |
| #print smt_tactic.slift_aux /- def missing doc string -/ | |
| #print smt_tactic.trace_state /- def missing doc string -/ | |
| #print smt_tactic.trace /- def missing doc string -/ | |
| #print smt_tactic.to_expr /- def missing doc string -/ | |
| #print smt_tactic.classical /- def missing doc string -/ | |
| #print smt_tactic.num_goals /- def missing doc string -/ | |
| #print smt_tactic.get_goals /- def missing doc string -/ | |
| #print smt_tactic.set_goals /- def missing doc string -/ | |
| #print smt_tactic.focus1 /- def missing doc string -/ | |
| #print smt_tactic.solve1 /- def missing doc string -/ | |
| #print smt_tactic.swap /- def missing doc string -/ | |
| #print smt_tactic.destruct /- def missing doc string -/ | |
| #print smt_tactic.by_cases /- def missing doc string -/ | |
| #print smt_tactic.by_contradiction /- def missing doc string -/ | |
| #print smt_tactic.get_facts /- def missing doc string -/ | |
| #print smt_tactic.get_refuted_facts /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_lemma /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_lhs_lemma /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_lemma_from_decl /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_lhs_lemma_from_decl /- def missing doc string -/ | |
| #print smt_tactic.add_ematch_eqn_lemmas_for /- def missing doc string -/ | |
| #print smt_tactic.add_lemmas_from_facts_core /- def missing doc string -/ | |
| #print smt_tactic.add_lemmas_from_facts /- def missing doc string -/ | |
| #print smt_tactic.induction /- def missing doc string -/ | |
| #print smt_tactic.when /- def missing doc string -/ | |
| #print smt_tactic.when_tracing /- def missing doc string -/ | |
| #print using_smt /- def missing doc string -/ | |
| #print using_smt_with /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/tactic.lean | |
| #print tactic_state /- constant missing doc string -/ | |
| #print tactic_state.env /- constant missing doc string -/ | |
| #print tactic_state.get_options /- constant missing doc string -/ | |
| #print tactic_state.set_options /- constant missing doc string -/ | |
| #print tactic_result /- def missing doc string -/ | |
| #print tactic.fail /- def missing doc string -/ | |
| #print tactic.up /- def missing doc string -/ | |
| #print tactic.down /- def missing doc string -/ | |
| #print interactive.executor.execute_explicit /- def missing doc string -/ | |
| #print interactive.executor.execute_with_explicit /- def missing doc string -/ | |
| #print tactic.try_lst /- def missing doc string -/ | |
| #print tactic.returnopt /- def missing doc string -/ | |
| #print tactic.get_options /- def missing doc string -/ | |
| #print tactic.set_options /- def missing doc string -/ | |
| #print tactic.save_options /- def missing doc string -/ | |
| #print tactic.returnex /- def missing doc string -/ | |
| #print tactic_format_expr /- def missing doc string -/ | |
| #print has_to_tactic_format /- constant missing doc string -/ | |
| #print tactic.pp /- def missing doc string -/ | |
| #print option_to_tactic_format /- def missing doc string -/ | |
| #print tactic.get_env /- def missing doc string -/ | |
| #print tactic.get_decl /- def missing doc string -/ | |
| #print tactic.trace /- def missing doc string -/ | |
| #print tactic.trace_call_stack /- def missing doc string -/ | |
| #print tactic.timetac /- def missing doc string -/ | |
| #print tactic.trace_state /- def missing doc string -/ | |
| #print tactic.intro_core /- constant missing doc string -/ | |
| #print tactic.intron /- constant missing doc string -/ | |
| #print tactic.subst_core /- constant missing doc string -/ | |
| #print tactic.mk_meta_univ /- constant missing doc string -/ | |
| #print tactic.mk_meta_var /- constant missing doc string -/ | |
| #print tactic.save_info_thunk /- constant missing doc string -/ | |
| #print tactic.frozen_local_instances /- constant missing doc string -/ | |
| #print tactic.induction' /- def missing doc string -/ | |
| #print tactic.istep /- def missing doc string -/ | |
| #print tactic.is_prop /- def missing doc string -/ | |
| #print tactic.is_proof /- def missing doc string -/ | |
| #print tactic.whnf_no_delta /- def missing doc string -/ | |
| #print tactic.whnf_target /- def missing doc string -/ | |
| #print tactic.introv /- def missing doc string -/ | |
| #print tactic.to_expr_strict /- def missing doc string -/ | |
| #print tactic.revert_all /- def missing doc string -/ | |
| #print tactic.clear_lst /- def missing doc string -/ | |
| #print tactic.match_not /- def missing doc string -/ | |
| #print tactic.match_and /- def missing doc string -/ | |
| #print tactic.match_or /- def missing doc string -/ | |
| #print tactic.match_iff /- def missing doc string -/ | |
| #print tactic.match_eq /- def missing doc string -/ | |
| #print tactic.match_ne /- def missing doc string -/ | |
| #print tactic.match_heq /- def missing doc string -/ | |
| #print tactic.match_refl_app /- def missing doc string -/ | |
| #print tactic.match_app_of /- def missing doc string -/ | |
| #print tactic.get_local_type /- def missing doc string -/ | |
| #print tactic.trace_result /- def missing doc string -/ | |
| #print tactic.rexact /- def missing doc string -/ | |
| #print tactic.any_hyp_aux /- def missing doc string -/ | |
| #print tactic.any_hyp /- def missing doc string -/ | |
| #print tactic.find_assumption /- def missing doc string -/ | |
| #print tactic.assumption /- def missing doc string -/ | |
| #print tactic.save_info /- def missing doc string -/ | |
| #print tactic.focus1 /- def missing doc string -/ | |
| #print tactic.is_trace_enabled_for /- constant missing doc string -/ | |
| #print tactic.apply_opt_param /- def missing doc string -/ | |
| #print tactic.apply_auto_param /- def missing doc string -/ | |
| #print tactic.has_opt_auto_param /- def missing doc string -/ | |
| #print tactic.try_apply_opt_auto_param /- def missing doc string -/ | |
| #print tactic.has_opt_auto_param_for_apply /- def missing doc string -/ | |
| #print tactic.try_apply_opt_auto_param_for_apply /- def missing doc string -/ | |
| #print tactic.apply /- def missing doc string -/ | |
| #print tactic.eapplyc /- def missing doc string -/ | |
| #print tactic.save_const_type_info /- def missing doc string -/ | |
| #print tactic.mk_local' /- def missing doc string -/ | |
| #print tactic.mk_local_def /- def missing doc string -/ | |
| #print tactic.mk_local_pis /- def missing doc string -/ | |
| #print tactic.triv /- def missing doc string -/ | |
| #print tactic.by_contradiction /- def missing doc string -/ | |
| #print tactic.generalizes /- def missing doc string -/ | |
| #print tactic.revert_kdeps /- def missing doc string -/ | |
| #print tactic.by_cases /- def missing doc string -/ | |
| #print tactic.funext_core /- def missing doc string -/ | |
| #print tactic.funext /- def missing doc string -/ | |
| #print tactic.funext_lst /- def missing doc string -/ | |
| #print tactic.new_aux_decl_name /- def missing doc string -/ | |
| #print tactic.abstract /- def missing doc string -/ | |
| #print tactic.updateex_env /- def missing doc string -/ | |
| #print tactic.add_inductive /- def missing doc string -/ | |
| #print tactic.add_meta_definition /- def missing doc string -/ | |
| #print tactic.main_goal /- def missing doc string -/ | |
| #print tactic.with_enable_tags /- def missing doc string -/ | |
| #print tactic.get_main_tag /- def missing doc string -/ | |
| #print tactic.set_main_tag /- def missing doc string -/ | |
| #print tactic.subst /- def missing doc string -/ | |
| #print list.for_each /- def missing doc string -/ | |
| #print list.any_of /- def missing doc string -/ | |
| #print monad_from_pure_bind /- def missing doc string -/ | |
| #print tactic.mk_id_proof /- def missing doc string -/ | |
| #print tactic.mk_id_eq /- def missing doc string -/ | |
| #print tactic.replace_target /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/task.lean | |
| #print task.get /- constant missing doc string -/ | |
| #print task.pure /- constant missing doc string -/ | |
| #print task.map /- constant missing doc string -/ | |
| #print task.flatten /- constant missing doc string -/ | |
| #print task.bind /- def missing doc string -/ | |
| #print task.delay /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/type_context.lean | |
| #print tactic.unsafe.type_context.bind /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.pure /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.fail /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.failure /- def missing doc string -/ | |
| #print tactic.unsafe.type_context.get_env /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.whnf /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.is_def_eq /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.unify /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.pop_local /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.list_mvars /- def missing doc string -/ | |
| #print tactic.unsafe.type_context.is_assigned /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.instantiate_mvars /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.level.instantiate_mvars /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.is_tmp_mvar /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.is_regular_mvar /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.tmp_is_assigned /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.tmp_get_assignment /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.level.tmp_is_assigned /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.level.tmp_get_assignment /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.mk_tmp_mvar /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.level.mk_tmp_mvar /- constant missing doc string -/ | |
| #print tactic.unsafe.type_context.orelse /- def missing doc string -/ | |
| #print tactic.unsafe.type_context.trace /- def missing doc string -/ | |
| #print tactic.unsafe.type_context.print_mvars /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/vm.lean | |
| #print vm_obj /- constant missing doc string -/ | |
| #print vm_obj_kind /- constant missing doc string -/ | |
| #print vm_obj.kind /- constant missing doc string -/ | |
| #print vm_decl /- constant missing doc string -/ | |
| #print vm_decl_kind /- constant missing doc string -/ | |
| #print vm_decl.kind /- constant missing doc string -/ | |
| #print vm_decl.to_name /- constant missing doc string -/ | |
| #print vm_core /- constant missing doc string -/ | |
| #print vm_core.map /- constant missing doc string -/ | |
| #print vm_core.ret /- constant missing doc string -/ | |
| #print vm_core.bind /- constant missing doc string -/ | |
| #print vm /- def missing doc string -/ | |
| #print vm.get_env /- constant missing doc string -/ | |
| #print vm.get_override /- def missing doc string -/ | |
| #print vm.get_options /- constant missing doc string -/ | |
| #print vm.stack_size /- constant missing doc string -/ | |
| #print vm.put_str /- constant missing doc string -/ | |
| #print vm.get_line /- constant missing doc string -/ | |
| #print vm.trace /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/well_founded_tactics.lean | |
| #print well_founded_tactics.clear_internals /- def missing doc string -/ | |
| #print well_founded_tactics.unfold_wf_rel /- def missing doc string -/ | |
| #print well_founded_tactics.is_psigma_mk /- def missing doc string -/ | |
| #print well_founded_tactics.process_lex /- def missing doc string -/ | |
| #print well_founded_tactics.unfold_sizeof /- def missing doc string -/ | |
| #print well_founded_tactics.cancel_nat_add_lt /- def missing doc string -/ | |
| #print well_founded_tactics.check_target_is_value_lt /- def missing doc string -/ | |
| #print well_founded_tactics.trivial_nat_lt /- def missing doc string -/ | |
| #print well_founded_tactics.default_dec_tac /- def missing doc string -/ | |
| #print well_founded_tactics.default /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/propext.lean | |
| #print propext /- constant missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/util.lean | |
| #print trace_val /- def missing doc string -/ | |
| #print undefined /- def missing doc string -/ | |
| #print unchecked_cast /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/version.lean | |
| #print lean.version /- def missing doc string -/ | |
| #print lean.githash /- def missing doc string -/ | |
| #print lean.is_release /- def missing doc string -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/wf.lean | |
| #print acc /- constant missing doc string -/ | |
| #print acc.inv /- def missing doc string -/ | |
| #print has_well_founded /- constant missing doc string -/ | |
| #print well_founded.apply /- def missing doc string -/ | |
| #print well_founded.fix_F /- def missing doc string -/ | |
| #print subrelation.accessible /- def missing doc string -/ | |
| #print subrelation.wf /- def missing doc string -/ | |
| #print inv_image.accessible /- def missing doc string -/ | |
| #print inv_image.wf /- def missing doc string -/ | |
| #print tc.accessible /- def missing doc string -/ | |
| #print tc.wf /- def missing doc string -/ | |
| #print measure /- def missing doc string -/ | |
| #print measure_wf /- def missing doc string -/ | |
| #print sizeof_measure /- def missing doc string -/ | |
| #print sizeof_measure_wf /- def missing doc string -/ | |
| #print prod.lex /- constant missing doc string -/ | |
| #print prod.rprod /- constant missing doc string -/ | |
| #print prod.lex_accessible /- def missing doc string -/ | |
| #print prod.lex_wf /- def missing doc string -/ | |
| #print prod.rprod_sub_lex /- def missing doc string -/ | |
| #print prod.rprod_wf /- def missing doc string -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/control/basic.lean | |
| #print mzip_with /- def missing doc string -/ | |
| #print mzip_with' /- def missing doc string -/ | |
| #print list.mpartition /- def missing doc string -/ | |
| #print list.mmap_accumr /- def missing doc string -/ | |
| #print list.mmap_accuml /- def missing doc string -/ | |
| #print succeeds /- def missing doc string -/ | |
| #print mtry /- def missing doc string -/ | |
| #print sum.bind /- def missing doc string -/ | |
| #print is_comm_applicative /- constant missing doc string -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/data/dlist/basic.lean | |
| #print dlist.join /- def missing doc string -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/data/list/defs.lean | |
| #print list.insert_nth /- def missing doc string -/ | |
| #print list.scanr_aux /- def missing doc string -/ | |
| #print list.partition_map /- def missing doc string -/ | |
| #print list.find_indexes_aux /- def missing doc string -/ | |
| #print list.map_with_index_core /- def missing doc string -/ | |
| #print list.sublists'_aux /- def missing doc string -/ | |
| #print list.sublists_aux /- def missing doc string -/ | |
| #print list.sublists_aux₁ /- def missing doc string -/ | |
| #print list.forall₂ /- constant missing doc string -/ | |
| #print list.transpose_aux /- def missing doc string -/ | |
| #print list.permutations_aux2 /- def missing doc string -/ | |
| #print list.permutations_aux.rec /- def missing doc string -/ | |
| #print list.permutations_aux /- def missing doc string -/ | |
| #print list.erasep /- def missing doc string -/ | |
| #print list.extractp /- def missing doc string -/ | |
| #print list.revzip /- def missing doc string -/ | |
| #print list.of_fn_aux /- def missing doc string -/ | |
| #print list.of_fn /- def missing doc string -/ | |
| #print list.of_fn_nth_val /- def missing doc string -/ | |
| #print list.traverse /- def missing doc string -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/data/option/defs.lean | |
| #print option.to_list /- def missing doc string -/ | |
| #print option.lift_or_get /- def missing doc string -/ | |
| #print option.rel /- constant missing doc string -/ | |
| #print option.traverse /- def missing doc string -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/logic/basic.lean | |
| #print hidden /- def missing doc string -/ | |
| #print empty.elim /- def missing doc string -/ | |
| #print pempty.elim /- def missing doc string -/ | |
| #print not.elim /- def missing doc string -/ | |
| #print decidable_of_iff /- def missing doc string -/ | |
| #print decidable_of_iff' /- def missing doc string -/ | |
| #print decidable_of_bool /- def missing doc string -/ | |
| #print classical.exists_cases /- def missing doc string -/ | |
| #print exists.classical_rec_on /- def missing doc string -/ | |
| /- The `unused_arguments` linter reports: -/ | |
| /- UNUSED ARGUMENTS: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/classes.lean | |
| #print strict_weak_order.esymm /- argument 3: [_inst_1 : is_strict_weak_order α r] -/ | |
| #print strict_weak_order.not_lt_of_equiv /- argument 3: [_inst_1 : is_strict_weak_order α r] -/ | |
| #print strict_weak_order.not_lt_of_equiv' /- argument 3: [_inst_1 : is_strict_weak_order α r] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/combinators.lean | |
| #print list.mfirst /- argument 2: [_inst_1 : monad m] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print except_t.monad_map /- argument 3: [_inst_1 : monad m], argument 5: [_inst_2 : monad m'] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad_fail.lean | |
| #print monad_fail_lift /- argument 3: [_inst_1 : monad n] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/option.lean | |
| #print option_t.monad_map /- argument 2: [_inst_1 : monad m], argument 4: [_inst_2 : monad m'] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print reader_t.lift /- argument 3: [_inst_1 : monad m] -/ | |
| #print reader_t.monad_map /- argument 4: [_inst_2 : monad m], argument 5: [_inst_3 : monad m'] -/ | |
| #print reader_t.adapt /- argument 3: [_inst_1 : monad m] (duplicate), argument 5: [_inst_2 : monad m] (duplicate) -/ | |
| #print reader_t.orelse /- argument 3: [_inst_1 : monad m] -/ | |
| #print reader_t.failure /- argument 3: [_inst_1 : monad m] -/ | |
| #print reader_t.monad_except /- argument 3: [_inst_1 : monad m] (duplicate) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print state_t.orelse /- argument 3: [_inst_1 : monad m] -/ | |
| #print state_t.failure /- argument 3: [_inst_1 : monad m] -/ | |
| #print state_t.monad_map /- argument 4: [_inst_2 : monad m], argument 5: [_inst_3 : monad m'] -/ | |
| #print get /- argument 3: [_inst_1 : monad m] -/ | |
| #print put /- argument 3: [_inst_1 : monad m] -/ | |
| #print modify /- argument 3: [_inst_1 : monad m] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/core.lean | |
| #print opt_param /- argument 2: (default : α) -/ | |
| #print combinator.K /- argument 4: (b : β) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/prod.lean | |
| #print prod_has_decidable_lt /- argument 6: [_inst_4 : decidable_eq β] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/function.lean | |
| #print function.const /- argument 4: (a : β) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print empty_relation /- argument 2: (a₁ : α) (duplicate), argument 3: (a₂ : α) (duplicate) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/interaction_monad.lean | |
| #print interaction_monad.mk_exception /- argument 6: (ref : option expr) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/interactive_base.lean | |
| #print interactive.parse /- argument 3: [_inst_1 : p.reflectable] -/ | |
| #print interactive.with_desc /- argument 2: (desc : format) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/name.lean | |
| #print auto_param /- argument 2: (tac_name : name) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/smt/interactive.lean | |
| #print smt_tactic.istep /- argument 3: (col0 : ℕ) (duplicate) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/tactic.lean | |
| #print tactic.istep /- argument 3: (col0 : ℕ) (duplicate) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/util.lean | |
| #print timeit /- argument 2: (s : string) -/ | |
| #print trace /- argument 2: (s : string) -/ | |
| #print scope_trace /- argument 2: {line : ℕ} (duplicate), argument 3: {col : ℕ} (duplicate) -/ | |
| #print try_for /- argument 2: (max : ℕ) -/ | |
| -- /Users/chb/Documents/lean/mathlib/src/tactic/core.lean | |
| #print tactic.symmetry_hyp /- argument 2: (md : opt_param transparency transparency.semireducible) -/ | |
| /- The `dup_namespace` linter reports: -/ | |
| /- DUPLICATED NAMESPACES IN NAME: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/comp_lemmas.lean | |
| #print int.int.zero_lt_one /- The namespace `int` is duplicated in the name -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/lemmas.lean | |
| #print nat.nat.lt_asymm /- The namespace `nat` is duplicated in the name -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/expr.lean | |
| #print expr.expr.lt_prop /- The namespace `expr` is duplicated in the name -/ | |
| /- The `ge_or_gt` linter reports: -/ | |
| /- USING ≥/> IN DECLARATIONS: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/order.lean | |
| #print ge_trans /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print gt_irrefl /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print gt_trans /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print gt.trans /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print gt_of_gt_of_ge /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print gt_of_ge_of_gt /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print lt_or_ge /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print le_or_gt /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print lt_or_gt_of_ne /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print ne_iff_lt_or_gt /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print lt_iff_not_ge /- the type contains ≥/>. Use ≤/< instead. -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/basic.lean | |
| #print int.nat_abs_pos_of_ne_zero /- the type contains ≥/>. Use ≤/< instead. -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/comp_lemmas.lean | |
| #print int.one_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.bit0_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.bit1_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.zero_nonneg /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.one_nonneg /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.bit0_nonneg /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.bit1_nonneg /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.nonneg_of_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print int.of_nat_ge_zero /- the type contains ≥/>. Use ≤/< instead. -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/order.lean | |
| #print int.coe_succ_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/lemmas.lean | |
| #print nat.eq_zero_or_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print nat.pos_of_ne_zero /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print nat.lt_or_ge /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print nat.sub_pos_of_lt /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print nat.mul_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| #print nat.pos_of_dvd_of_pos /- the type contains ≥/>. Use ≤/< instead. -/ | |
| /- The `has_coe_to_fun` linter reports: -/ | |
| /- INVALID/MISSING `has_coe_to_fun` instances. | |
| You should add a `has_coe_to_fun` instance for the following types. | |
| See Note function coercions].: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/expr.lean | |
| #print reflected /- `has_coe_to_fun` instance is definitionally equal to a transitive instance composed of: | |
| @expr.has_coe_to_fun bool.tt | |
| and | |
| @coe_base_aux.{1 1} (@reflected.{u} α a) (expr bool.tt) (@expr.has_coe.{u} α a) -/ | |
| /- The `decidable_classical` linter reports: -/ | |
| /- USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF.: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/classes.lean | |
| #print is_strict_weak_order_of_is_total_preorder /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 4: [_inst_1 : decidable_rel le] -/ | |
| #print lt_of_lt_of_incomp /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 4: [_inst_2 : decidable_rel lt] -/ | |
| #print lt_of_incomp_of_lt /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 4: [_inst_2 : decidable_rel lt] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/basic.lean | |
| #print list.lt_eq_not_ge /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 3: [_inst_2 : decidable_rel has_lt.lt] -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print decidable.em /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 2: [_inst_1 : decidable p] -/ | |
| #print decidable.by_contradiction /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 2: [_inst_1 : decidable p] -/ | |
| #print decidable.of_not_not /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 2: [_inst_1 : decidable p] -/ | |
| #print decidable.not_not_iff /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 2: [_inst_1 : decidable p] -/ | |
| #print decidable.not_and_iff_or_not /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 3: [d₁ : decidable p], argument 4: [d₂ : decidable q] -/ | |
| #print decidable.not_or_iff_and_not /- The following `decidable` hypotheses should be replaced with | |
| `classical` in the proof. argument 3: [d₁ : decidable p], argument 4: [d₂ : decidable q] -/ | |
| /- The `inhabited_nonempty` linter reports: -/ | |
| /- USES OF `inhabited` SHOULD BE REPLACED WITH `nonempty`.: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print nonempty_of_inhabited /- The following `inhabited` instances should be `nonempty`. argument 2: [_inst_1 : inhabited α] -/ | |
| /- OK: No invalid `has_coe` instances. -/ | |
| /- The `fails_quickly` linter reports: -/ | |
| /- TYPE CLASS SEARCHES TIMED OUT. | |
| For the following classes, there is an instance that causes a loop, or an excessively long search.: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print monad_except_adapter /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances') -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print monad_reader_adapter /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances') -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print monad_state /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances') -/ | |
| #print monad_state_adapter /- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances') -/ | |
| /- The `dangerous_instance` linter reports: -/ | |
| /- DANGEROUS INSTANCES FOUND. | |
| These instances are recursive, and create a new type-class problem which will have metavariables. | |
| Possible solution: remove the instance attribute or make it a local instance instead. | |
| Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive.: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/coe.lean | |
| #print lift_trans /- The following arguments become metavariables. argument 2: {b : Sort u₂} -/ | |
| #print coe_trans /- The following arguments become metavariables. argument 2: {b : Sort u₂} -/ | |
| #print coe_trans_aux /- The following arguments become metavariables. argument 2: {b : Sort u₂} -/ | |
| #print coe_fn_trans /- The following arguments become metavariables. argument 2: {b : Sort u₂} -/ | |
| #print coe_sort_trans /- The following arguments become metavariables. argument 2: {b : Sort u₂} -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print monad_except_adapter_trans /- The following arguments become metavariables. argument 3: {m : Type u → Type v}, argument 4: {m' : Type u → Type v} -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/lift.lean | |
| #print has_monad_lift_t_trans /- The following arguments become metavariables. argument 2: (n : Type u_1 → Type u_3) -/ | |
| #print monad_functor_t_trans /- The following arguments become metavariables. argument 3: (n : Type u_1 → Type u_3), argument 4: (n' : Type u_1 → Type u_3) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad_fail.lean | |
| #print monad_fail_lift /- The following arguments become metavariables. argument 1: (m : Type u → Type v) -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print monad_reader_trans /- The following arguments become metavariables. argument 2: {m : Type u → Type v} -/ | |
| #print monad_reader_adapter_trans /- The following arguments become metavariables. argument 3: {m : Type u → Type v}, argument 4: {m' : Type u → Type v} -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print monad_state_trans /- The following arguments become metavariables. argument 2: {m : Type u → Type v} -/ | |
| #print monad_state_adapter_trans /- The following arguments become metavariables. argument 3: {m : Type u → Type v}, argument 4: {m' : Type u → Type v} -/ | |
| /- OK: All declarations have correct type-class arguments. -/ | |
| /- The `impossible_instance` linter reports: -/ | |
| /- IMPOSSIBLE INSTANCES FOUND. | |
| These instances have an argument that cannot be found during type-class resolution, and therefore can never succeed. Either mark the arguments with square brackets (if it is a class), or don't make it an instance: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/subtype/basic.lean | |
| #print subtype.inhabited /- Impossible to infer argument 4: (h : p a) -/ | |
| /- The `has_inhabited_instance` linter reports: -/ | |
| /- TYPES ARE MISSING INHABITED INSTANCES: -/ | |
| -- | |
| #print quot /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/data/dlist.lean | |
| #print dlist /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print except /- inhabited instance missing -/ | |
| #print except_t /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/option.lean | |
| #print option_t /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print reader_t /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print state_t /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/core.lean | |
| #print empty /- inhabited instance missing -/ | |
| #print sigma /- inhabited instance missing -/ | |
| #print psigma /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/array/basic.lean | |
| #print d_array /- inhabited instance missing -/ | |
| #print array /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/fin/basic.lean | |
| #print fin /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/int/basic.lean | |
| #print int /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/quot.lean | |
| #print quotient /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/set.lean | |
| #print set /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/case_tag.lean | |
| #print tactic.interactive.case_tag /- inhabited instance missing -/ | |
| #print tactic.interactive.case_tag.match_result /- inhabited instance missing -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/tactic.lean | |
| #print tactic.tag /- inhabited instance missing -/ | |
| /- The `instance_priority` linter reports: -/ | |
| /- DANGEROUS INSTANCE PRIORITIES. | |
| The following instances always apply, and therefore should have a priority < 1000. | |
| If you don't know what priority to choose, use priority 100. | |
| If this is an automatically generated instance (using the keywords `class` and `extends`), | |
| see note [lower instance priority] and see note [default priority] for instructions to change the priority: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/algebra/classes.lean | |
| #print is_symm_op_of_is_commutative /- set priority below 1000 -/ | |
| #print is_symm_op_of_is_symm /- set priority below 1000 -/ | |
| #print is_preorder.to_is_refl /- set priority below 1000 -/ | |
| #print is_preorder.to_is_trans /- set priority below 1000 -/ | |
| #print is_total_preorder.to_is_total /- set priority below 1000 -/ | |
| #print is_total_preorder.to_is_trans /- set priority below 1000 -/ | |
| #print is_total_preorder_is_preorder /- set priority below 1000 -/ | |
| #print is_partial_order.to_is_antisymm /- set priority below 1000 -/ | |
| #print is_partial_order.to_is_preorder /- set priority below 1000 -/ | |
| #print is_linear_order.to_is_total /- set priority below 1000 -/ | |
| #print is_linear_order.to_is_partial_order /- set priority below 1000 -/ | |
| #print is_equiv.to_is_preorder /- set priority below 1000 -/ | |
| #print is_equiv.to_is_symm /- set priority below 1000 -/ | |
| #print is_per.to_is_trans /- set priority below 1000 -/ | |
| #print is_per.to_is_symm /- set priority below 1000 -/ | |
| #print is_strict_order.to_is_trans /- set priority below 1000 -/ | |
| #print is_strict_order.to_is_irrefl /- set priority below 1000 -/ | |
| #print is_strict_weak_order.to_is_strict_order /- set priority below 1000 -/ | |
| #print is_strict_weak_order.to_is_incomp_trans /- set priority below 1000 -/ | |
| #print is_strict_total_order.to_is_trichotomous /- set priority below 1000 -/ | |
| #print is_strict_total_order.to_is_strict_weak_order /- set priority below 1000 -/ | |
| #print is_asymm_of_is_trans_of_is_irrefl /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/coe.lean | |
| #print lift_trans /- set priority below 1000 -/ | |
| #print lift_base /- set priority below 1000 -/ | |
| #print coe_trans /- set priority below 1000 -/ | |
| #print coe_base /- set priority below 1000 -/ | |
| #print coe_trans_aux /- set priority below 1000 -/ | |
| #print coe_base_aux /- set priority below 1000 -/ | |
| #print coe_fn_trans /- set priority below 1000 -/ | |
| #print coe_sort_trans /- set priority below 1000 -/ | |
| #print coe_to_lift /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/alternative.lean | |
| #print alternative.to_has_orelse /- set priority below 1000 -/ | |
| #print alternative.to_applicative /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/applicative.lean | |
| #print applicative.to_has_seq_left /- set priority below 1000 -/ | |
| #print applicative.to_has_seq /- set priority below 1000 -/ | |
| #print applicative.to_has_pure /- set priority below 1000 -/ | |
| #print applicative.to_functor /- set priority below 1000 -/ | |
| #print applicative.to_has_seq_right /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/except.lean | |
| #print monad_except_adapter_trans /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/lawful.lean | |
| #print is_lawful_applicative.to_is_lawful_functor /- set priority below 1000 -/ | |
| #print is_lawful_monad.to_is_lawful_applicative /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/lift.lean | |
| #print has_monad_lift_t_trans /- set priority below 1000 -/ | |
| #print monad_functor_t_trans /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad.lean | |
| #print monad.to_applicative /- set priority below 1000 -/ | |
| #print monad.to_has_bind /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/monad_fail.lean | |
| #print monad_fail_lift /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/reader.lean | |
| #print monad_reader_trans /- set priority below 1000 -/ | |
| #print monad_reader_adapter_trans /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/control/state.lean | |
| #print monad_state_trans /- set priority below 1000 -/ | |
| #print monad_state_adapter_trans /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/core.lean | |
| #print default_has_sizeof /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/setoid.lean | |
| #print setoid_has_equiv /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print nonempty_of_inhabited /- set priority below 1000 -/ | |
| #print subsingleton_prop /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/meta/lean/parser.lean | |
| #print lean.parser.reflectable.has_reflect /- set priority below 1000 -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/wf.lean | |
| #print has_well_founded_of_has_sizeof /- set priority below 1000 -/ | |
| /- OK: No commutativity lemma is marked simp. -/ | |
| /- The `simp_var_head` linter reports: -/ | |
| /- LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL. | |
| Some simp lemmas have a variable as head symbol of the left-hand side: -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/lemmas.lean | |
| #print list.ball_nil /- Left-hand side has variable as head symbol: p -/ | |
| /- The `simp_nf` linter reports: -/ | |
| /- SOME SIMP LEMMAS ARE REDUNDANT. | |
| That is, their left-hand side is not in simp-normal form. | |
| These lemmas are hence never used by the simplifier. | |
| This linter gives you a list of other simp lemmas, look at them! | |
| Here are some guidelines to get you started: | |
| 1. 'the left-hand side reduces to XYZ': | |
| you should probably use XYZ as the left-hand side. | |
| 2. 'simp can prove this': | |
| This typically means that lemma is a duplicate, or is shadowed by another lemma: | |
| 2a. Always put more general lemmas after specific ones: | |
| @[simp] lemma zero_add_zero : 0 + 0 = 0 := rfl | |
| @[simp] lemma add_zero : x + 0 = x := rfl | |
| And not the other way around! The simplifier always picks the last matching lemma. | |
| 2b. You can also use @[priority] instead of moving simp-lemmas around in the file. | |
| Tip: the default priority is 1000. | |
| Use `@[priority 1100]` instead of moving a lemma down, | |
| and `@[priority 900]` instead of moving a lemma up. | |
| 2c. Conditional simp lemmas are tried last, if they are shadowed | |
| just remove the simp attribute. | |
| 2d. If two lemmas are duplicates, the linter will complain about the first one. | |
| Try to fix the second one instead! | |
| (You can find it among the other simp lemmas the linter prints out!) | |
| : -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/bool/lemmas.lean | |
| #print tt_eq_ff_eq_false /- simp can prove this: | |
| by simp only [] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print ff_eq_tt_eq_false /- simp can prove this: | |
| by simp only [] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print coe_sort_ff /- simp can prove this: | |
| by simp only [bool.coe_sort_ff] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print coe_sort_tt /- simp can prove this: | |
| by simp only [bool.coe_sort_tt] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/list/lemmas.lean | |
| #print list.mem_nil_iff /- simp can prove this: | |
| by simp only [list.not_mem_nil] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print list.mem_cons_self /- simp can prove this: | |
| by simp only [list.mem_cons_iff, true_or, eq_self_iff_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print list.not_bex_nil /- simp can prove this: | |
| by simp only [list.not_mem_nil, exists_false, not_false_iff, exists_prop_of_false] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print list.bex_cons /- Left-hand side simplifies from | |
| ∃ (x : α) (H : x ∈ a :: l), p x | |
| to | |
| ∃ (x : α), (x = a ∨ x ∈ l) ∧ p x | |
| using | |
| [exists_prop, list.mem_cons_iff] | |
| Try to change the left-hand side to the simplified term! | |
| -/ | |
| #print list.ball_cons /- Left-hand side simplifies from | |
| ∀ (x : α), x ∈ a :: l → p x | |
| to | |
| ∀ (x : α), x = a ∨ x ∈ l → p x | |
| using | |
| [list.mem_cons_iff] | |
| Try to change the left-hand side to the simplified term! | |
| -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/data/nat/bitwise.lean | |
| #print nat.bodd_one /- simp can prove this: | |
| by simp only [bnot, nat.bodd_succ, nat.bodd_zero, bool.bnot_false] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print nat.bodd_two /- simp can prove this: | |
| by simp only [bnot, nat.bodd_succ, nat.bodd_zero, bool.bnot_false, bool.bnot_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print nat.div2_one /- simp can prove this: | |
| by simp only [nat.div2_zero, nat.bodd_zero, bool.cond_ff, nat.div2_succ, cond] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print nat.div2_two /- Left-hand side simplifies from | |
| 2.div2 | |
| to | |
| 1 | |
| using | |
| [bnot, nat.bodd_succ, nat.div2_zero, nat.bodd_zero, bool.cond_ff, bool.cond_tt, bool.bnot_false, nat.div2_succ, cond] | |
| Try to change the left-hand side to the simplified term! | |
| -/ | |
| -- /Users/chb/.elan/toolchains/leanprover-community-lean-3.14.0/lib/lean/library/init/logic.lean | |
| #print ne_self_iff_false /- simp can prove this: | |
| by simp only [eq_self_iff_true, not_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print heq_self_iff_true /- simp can prove this: | |
| by simp only [eq_self_iff_true, heq_iff_eq] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print true_iff_false /- simp can prove this: | |
| by simp only [not_true, iff_false] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print false_iff_true /- simp can prove this: | |
| by simp only [false_iff, not_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print implies_true_iff /- simp can prove this: | |
| by simp only [forall_true_iff] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print false_implies_iff /- simp can prove this: | |
| by simp only [forall_prop_of_false, not_false_iff] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print true_implies_iff /- simp can prove this: | |
| by simp only [forall_prop_of_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print to_bool_true_eq_tt /- simp can prove this: | |
| by simp only [bool.to_bool_true] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ | |
| #print to_bool_false_eq_ff /- simp can prove this: | |
| by simp only [bool.to_bool_false] | |
| One of the lemmas above could be a duplicate. | |
| If that's not the case try reordering lemmas or adding @[priority]. | |
| -/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment