Created
August 2, 2020 04:55
-
-
Save r-ryantm/bc35cecad7f11eb9cb377ac7279dcd74 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
| /nix/store/06wclm0wwn8161mr4zjf6aa497385ld9-lean-3.18.4 | |
| ├── bin | |
| │ ├── lean | |
| │ ├── leanchecker | |
| │ └── leanpkg | |
| ├── include | |
| │ └── lean_ext | |
| │ ├── build | |
| │ │ ├── checker | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── leanchecker.dir | |
| │ │ ├── CMakeFiles | |
| │ │ │ ├── 3.17.3 | |
| │ │ │ │ ├── CompilerIdC | |
| │ │ │ │ │ └── tmp | |
| │ │ │ │ └── CompilerIdCXX | |
| │ │ │ │ └── tmp | |
| │ │ │ ├── clean-leanpkg.dir | |
| │ │ │ ├── clean-olean.dir | |
| │ │ │ ├── clean-std-lib.dir | |
| │ │ │ ├── CMakeTmp | |
| │ │ │ └── leanstatic.dir | |
| │ │ ├── frontends | |
| │ │ │ └── lean | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── lean_frontend.dir | |
| │ │ ├── githash.h | |
| │ │ ├── init | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── init.dir | |
| │ │ ├── kernel | |
| │ │ │ ├── CMakeFiles | |
| │ │ │ │ └── kernel.dir | |
| │ │ │ ├── inductive | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── inductive.dir | |
| │ │ │ └── quotient | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── quotient.dir | |
| │ │ ├── library | |
| │ │ │ ├── CMakeFiles | |
| │ │ │ │ └── library.dir | |
| │ │ │ ├── compiler | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── compiler.dir | |
| │ │ │ ├── constructions | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── constructions.dir | |
| │ │ │ ├── equations_compiler | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── equations_compiler.dir | |
| │ │ │ ├── inductive_compiler | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── inductive_compiler.dir | |
| │ │ │ ├── tactic | |
| │ │ │ │ ├── backward | |
| │ │ │ │ │ └── CMakeFiles | |
| │ │ │ │ │ └── backward.dir | |
| │ │ │ │ ├── CMakeFiles | |
| │ │ │ │ │ └── tactic.dir | |
| │ │ │ │ └── smt | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── smt.dir | |
| │ │ │ └── vm | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── vm.dir | |
| │ │ ├── shell | |
| │ │ │ └── CMakeFiles | |
| │ │ │ ├── bin_lean.dir | |
| │ │ │ ├── lean.dir | |
| │ │ │ ├── lean_js.dir | |
| │ │ │ └── shell_js.dir | |
| │ │ ├── tests | |
| │ │ │ └── shell | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── shell_test.dir | |
| │ │ ├── util | |
| │ │ │ ├── CMakeFiles | |
| │ │ │ │ └── util.dir | |
| │ │ │ ├── numerics | |
| │ │ │ │ └── CMakeFiles | |
| │ │ │ │ └── numerics.dir | |
| │ │ │ └── sexpr | |
| │ │ │ └── CMakeFiles | |
| │ │ │ └── sexpr.dir | |
| │ │ └── version.h | |
| │ ├── checker | |
| │ │ ├── simple_pp.h | |
| │ │ └── text_import.h | |
| │ ├── cmake | |
| │ │ └── Modules | |
| │ ├── frontends | |
| │ │ └── lean | |
| │ │ ├── brackets.h | |
| │ │ ├── builtin_cmds.h | |
| │ │ ├── builtin_exprs.h | |
| │ │ ├── calc.h | |
| │ │ ├── cmd_table.h | |
| │ │ ├── completion.h | |
| │ │ ├── decl_attributes.h | |
| │ │ ├── decl_cmds.h | |
| │ │ ├── decl_util.h | |
| │ │ ├── definition_cmds.h | |
| │ │ ├── dependencies.h | |
| │ │ ├── elaborator.h | |
| │ │ ├── inductive_cmds.h | |
| │ │ ├── info_manager.h | |
| │ │ ├── init_module.h | |
| │ │ ├── interactive.h | |
| │ │ ├── json.h | |
| │ │ ├── local_context_adapter.h | |
| │ │ ├── local_decls.h | |
| │ │ ├── local_level_decls.h | |
| │ │ ├── match_expr.h | |
| │ │ ├── module_parser.h | |
| │ │ ├── notation_cmd.h | |
| │ │ ├── parser_config.h | |
| │ │ ├── parser.h | |
| │ │ ├── parser_pos_provider.h | |
| │ │ ├── parser_state.h | |
| │ │ ├── parse_table.h | |
| │ │ ├── pp.h | |
| │ │ ├── prenum.h | |
| │ │ ├── print_cmd.h | |
| │ │ ├── scanner.h | |
| │ │ ├── structure_cmd.h | |
| │ │ ├── structure_instance.h | |
| │ │ ├── tactic_notation.h | |
| │ │ ├── tokens.h | |
| │ │ ├── token_table.h | |
| │ │ ├── type_util.h | |
| │ │ ├── user_command.h | |
| │ │ ├── user_notation.h | |
| │ │ ├── util.h | |
| │ │ └── widget.h | |
| │ ├── init | |
| │ │ └── init.h | |
| │ ├── kernel | |
| │ │ ├── abstract.h | |
| │ │ ├── abstract_type_context.h | |
| │ │ ├── cache_stack.h | |
| │ │ ├── declaration.h | |
| │ │ ├── environment.h | |
| │ │ ├── equiv_manager.h | |
| │ │ ├── error_msgs.h | |
| │ │ ├── expr_cache.h | |
| │ │ ├── expr_eq_fn.h | |
| │ │ ├── expr.h | |
| │ │ ├── expr_maps.h | |
| │ │ ├── expr_pair.h | |
| │ │ ├── expr_sets.h | |
| │ │ ├── ext_exception.h | |
| │ │ ├── find_fn.h | |
| │ │ ├── for_each_fn.h | |
| │ │ ├── formatter.h | |
| │ │ ├── free_vars.h | |
| │ │ ├── inductive | |
| │ │ │ └── inductive.h | |
| │ │ ├── init_module.h | |
| │ │ ├── instantiate.h | |
| │ │ ├── kernel_exception.h | |
| │ │ ├── level.h | |
| │ │ ├── normalizer_extension.h | |
| │ │ ├── pos_info_provider.h | |
| │ │ ├── quotient | |
| │ │ │ └── quotient.h | |
| │ │ ├── replace_fn.h | |
| │ │ ├── scope_pos_info_provider.h | |
| │ │ ├── standard_kernel.h | |
| │ │ └── type_checker.h | |
| │ ├── library | |
| │ │ ├── abstract_context_cache.h | |
| │ │ ├── abstract_parser.h | |
| │ │ ├── ac_match.h | |
| │ │ ├── aliases.h | |
| │ │ ├── annotation.h | |
| │ │ ├── app_builder.h | |
| │ │ ├── attribute_manager.h | |
| │ │ ├── aux_definition.h | |
| │ │ ├── aux_recursors.h | |
| │ │ ├── bin_app.h | |
| │ │ ├── cache_helper.h | |
| │ │ ├── check.h | |
| │ │ ├── choice.h | |
| │ │ ├── class.h | |
| │ │ ├── compiler | |
| │ │ │ ├── compiler_step_visitor.h | |
| │ │ │ ├── comp_irrelevant.h | |
| │ │ │ ├── cse.h | |
| │ │ │ ├── elim_recursors.h | |
| │ │ │ ├── elim_unused_lets.h | |
| │ │ │ ├── erase_irrelevant.h | |
| │ │ │ ├── eta_expansion.h | |
| │ │ │ ├── extract_values.h | |
| │ │ │ ├── init_module.h | |
| │ │ │ ├── inliner.h | |
| │ │ │ ├── lambda_lifting.h | |
| │ │ │ ├── nat_value.h | |
| │ │ │ ├── preprocess.h | |
| │ │ │ ├── procedure.h | |
| │ │ │ ├── rec_fn_macro.h | |
| │ │ │ ├── reduce_arity.h | |
| │ │ │ ├── simp_inductive.h | |
| │ │ │ ├── util.h | |
| │ │ │ └── vm_compiler.h | |
| │ │ ├── comp_val.h | |
| │ │ ├── congr_lemma.h | |
| │ │ ├── constants.h | |
| │ │ ├── constructions | |
| │ │ │ ├── brec_on.h | |
| │ │ │ ├── cases_on.h | |
| │ │ │ ├── constructor.h | |
| │ │ │ ├── drec.h | |
| │ │ │ ├── has_sizeof.h | |
| │ │ │ ├── init_module.h | |
| │ │ │ ├── injective.h | |
| │ │ │ ├── no_confusion.h | |
| │ │ │ ├── projection.h | |
| │ │ │ ├── rec_on.h | |
| │ │ │ └── util.h | |
| │ │ ├── context_cache.h | |
| │ │ ├── deep_copy.h | |
| │ │ ├── defeq_canonizer.h | |
| │ │ ├── delayed_abstraction.h | |
| │ │ ├── discr_tree.h | |
| │ │ ├── documentation.h | |
| │ │ ├── elab_context.h | |
| │ │ ├── equations_compiler | |
| │ │ │ ├── compiler.h | |
| │ │ │ ├── elim_match.h | |
| │ │ │ ├── equations.h | |
| │ │ │ ├── init_module.h | |
| │ │ │ ├── pack_domain.h | |
| │ │ │ ├── pack_mutual.h | |
| │ │ │ ├── structural_rec.h | |
| │ │ │ ├── unbounded_rec.h | |
| │ │ │ ├── util.h | |
| │ │ │ └── wf_rec.h | |
| │ │ ├── eval_helper.h | |
| │ │ ├── exception.h | |
| │ │ ├── explicit.h | |
| │ │ ├── export_decl.h | |
| │ │ ├── export.h | |
| │ │ ├── expr_address.h | |
| │ │ ├── expr_lt.h | |
| │ │ ├── expr_pair.h | |
| │ │ ├── expr_pair_maps.h | |
| │ │ ├── expr_unsigned_map.h | |
| │ │ ├── fingerprint.h | |
| │ │ ├── fun_info.h | |
| │ │ ├── handle.h | |
| │ │ ├── head_map.h | |
| │ │ ├── idx_metavar.h | |
| │ │ ├── inductive_compiler | |
| │ │ │ ├── add_decl.h | |
| │ │ │ ├── basic.h | |
| │ │ │ ├── compiler.h | |
| │ │ │ ├── ginductive_decl.h | |
| │ │ │ ├── ginductive.h | |
| │ │ │ ├── init_module.h | |
| │ │ │ ├── mutual.h | |
| │ │ │ ├── nested.h | |
| │ │ │ └── util.h | |
| │ │ ├── init_module.h | |
| │ │ ├── inverse.h | |
| │ │ ├── io_state.h | |
| │ │ ├── io_state_stream.h | |
| │ │ ├── kernel_serializer.h | |
| │ │ ├── library_task_builder.h | |
| │ │ ├── local_context.h | |
| │ │ ├── local_instances.h | |
| │ │ ├── locals.h | |
| │ │ ├── max_sharing.h | |
| │ │ ├── message_builder.h | |
| │ │ ├── messages.h | |
| │ │ ├── metavar_context.h | |
| │ │ ├── metavar_util.h | |
| │ │ ├── module.h | |
| │ │ ├── module_mgr.h | |
| │ │ ├── mt_task_queue.h | |
| │ │ ├── native_compiler | |
| │ │ │ └── cpp_compiler.h | |
| │ │ ├── noncomputable.h | |
| │ │ ├── normalize.h | |
| │ │ ├── num.h | |
| │ │ ├── parray.h | |
| │ │ ├── pattern_attribute.h | |
| │ │ ├── persistent_context_cache.h | |
| │ │ ├── phash_map.h | |
| │ │ ├── phashtable.h | |
| │ │ ├── pipe.h | |
| │ │ ├── placeholder.h | |
| │ │ ├── pp_options.h | |
| │ │ ├── print.h | |
| │ │ ├── private.h | |
| │ │ ├── process.h | |
| │ │ ├── profiling.h | |
| │ │ ├── projection.h | |
| │ │ ├── protected.h | |
| │ │ ├── quote.h | |
| │ │ ├── reducible.h | |
| │ │ ├── relation_manager.h | |
| │ │ ├── replace_visitor.h | |
| │ │ ├── replace_visitor_with_tc.h | |
| │ │ ├── scoped_ext.h | |
| │ │ ├── shared_environment.h | |
| │ │ ├── sorry.h | |
| │ │ ├── string.h | |
| │ │ ├── st_task_queue.h | |
| │ │ ├── tactic | |
| │ │ │ ├── ac_tactics.h | |
| │ │ │ ├── algebraic_normalizer.h | |
| │ │ │ ├── app_builder_tactics.h | |
| │ │ │ ├── apply_tactic.h | |
| │ │ │ ├── assert_tactic.h | |
| │ │ │ ├── backward | |
| │ │ │ │ ├── backward_chaining.h | |
| │ │ │ │ ├── backward_lemmas.h | |
| │ │ │ │ └── init_module.h | |
| │ │ │ ├── cases_tactic.h | |
| │ │ │ ├── change_tactic.h | |
| │ │ │ ├── clear_tactic.h | |
| │ │ │ ├── congr_lemma_tactics.h | |
| │ │ │ ├── destruct_tactic.h | |
| │ │ │ ├── dsimplify.h | |
| │ │ │ ├── elaborate.h | |
| │ │ │ ├── elaborator_exception.h | |
| │ │ │ ├── eqn_lemmas.h | |
| │ │ │ ├── eval.h | |
| │ │ │ ├── exact_tactic.h | |
| │ │ │ ├── fun_info_tactics.h | |
| │ │ │ ├── generalize_tactic.h | |
| │ │ │ ├── gexpr.h | |
| │ │ │ ├── hole_command.h | |
| │ │ │ ├── hsubstitution.h | |
| │ │ │ ├── induction_tactic.h | |
| │ │ │ ├── init_module.h | |
| │ │ │ ├── intro_tactic.h | |
| │ │ │ ├── kabstract.h | |
| │ │ │ ├── match_tactic.h | |
| │ │ │ ├── occurrences.h | |
| │ │ │ ├── revert_tactic.h | |
| │ │ │ ├── rewrite_tactic.h | |
| │ │ │ ├── simp_lemmas.h | |
| │ │ │ ├── simplify.h | |
| │ │ │ ├── simp_result.h | |
| │ │ │ ├── simp_util.h | |
| │ │ │ ├── smt | |
| │ │ │ │ ├── congruence_closure.h | |
| │ │ │ │ ├── congruence_tactics.h | |
| │ │ │ │ ├── ematch.h | |
| │ │ │ │ ├── hinst_lemmas.h | |
| │ │ │ │ ├── init_module.h | |
| │ │ │ │ ├── smt_state.h | |
| │ │ │ │ ├── theory_ac.h | |
| │ │ │ │ └── util.h | |
| │ │ │ ├── subst_tactic.h | |
| │ │ │ ├── tactic_evaluator.h | |
| │ │ │ ├── tactic_state.h | |
| │ │ │ ├── unfold_tactic.h | |
| │ │ │ ├── user_attribute.h | |
| │ │ │ ├── vm_local_context.h | |
| │ │ │ ├── vm_monitor.h | |
| │ │ │ └── vm_type_context.h | |
| │ │ ├── time_task.h | |
| │ │ ├── trace.h | |
| │ │ ├── type_context.h | |
| │ │ ├── typed_expr.h | |
| │ │ ├── unfold_macros.h | |
| │ │ ├── unification_hint.h | |
| │ │ ├── unique_id.h | |
| │ │ ├── update_declaration.h | |
| │ │ ├── user_recursors.h | |
| │ │ ├── util.h | |
| │ │ └── vm | |
| │ │ ├── init_module.h | |
| │ │ ├── interaction_state.h | |
| │ │ ├── interaction_state_imp.h | |
| │ │ ├── optimize.h | |
| │ │ ├── vm_array.h | |
| │ │ ├── vm_aux.h | |
| │ │ ├── vm_declaration.h | |
| │ │ ├── vm_eformat.h | |
| │ │ ├── vm_environment.h | |
| │ │ ├── vm_exceptional.h | |
| │ │ ├── vm_expr.h | |
| │ │ ├── vm_float.h | |
| │ │ ├── vm_format.h | |
| │ │ ├── vm.h | |
| │ │ ├── vm_int.h | |
| │ │ ├── vm_io.h | |
| │ │ ├── vm_level.h | |
| │ │ ├── vm_list.h | |
| │ │ ├── vm_module_info.h | |
| │ │ ├── vm_name.h | |
| │ │ ├── vm_nat.h | |
| │ │ ├── vm_option.h | |
| │ │ ├── vm_options.h | |
| │ │ ├── vm_ordering.h | |
| │ │ ├── vm_override.h | |
| │ │ ├── vm_parser.h | |
| │ │ ├── vm_pexpr.h | |
| │ │ ├── vm_pos_info.h | |
| │ │ ├── vm_rb_map.h | |
| │ │ ├── vm_string.h | |
| │ │ └── vm_task.h | |
| │ ├── shared | |
| │ ├── shell | |
| │ │ ├── emscripten.h | |
| │ │ ├── leandoc.h | |
| │ │ ├── lean_js.h | |
| │ │ ├── server.h | |
| │ │ └── simple_pos_info_provider.h | |
| │ ├── tests | |
| │ │ ├── frontends | |
| │ │ │ └── lean | |
| │ │ ├── kernel | |
| │ │ ├── library | |
| │ │ │ └── rewriter | |
| │ │ ├── shell | |
| │ │ └── util | |
| │ │ └── numerics | |
| │ └── util | |
| │ ├── ascii.h | |
| │ ├── bitap_fuzzy_search.h | |
| │ ├── bit_tricks.h | |
| │ ├── buffer.h | |
| │ ├── cancellable.h | |
| │ ├── compiler_hints.h | |
| │ ├── debug.h | |
| │ ├── escaped.h | |
| │ ├── exception.h | |
| │ ├── exception_with_pos.h | |
| │ ├── extensible_object.h | |
| │ ├── file_lock.h | |
| │ ├── flet.h | |
| │ ├── freset.h | |
| │ ├── fresh_name.h | |
| │ ├── hash.h | |
| │ ├── init_module.h | |
| │ ├── int64.h | |
| │ ├── interrupt.h | |
| │ ├── lbool.h | |
| │ ├── lean_path.h | |
| │ ├── line_endings.h | |
| │ ├── list_fn.h | |
| │ ├── list.h | |
| │ ├── log_tree.h | |
| │ ├── lru_cache.h | |
| │ ├── macros.h | |
| │ ├── map.h | |
| │ ├── memory.h | |
| │ ├── memory_pool.h | |
| │ ├── message_definitions.h | |
| │ ├── name_generator.h | |
| │ ├── name.h | |
| │ ├── name_hash_map.h | |
| │ ├── name_hash_set.h | |
| │ ├── name_map.h | |
| │ ├── name_set.h | |
| │ ├── null_ostream.h | |
| │ ├── numerics | |
| │ │ ├── mpq.h | |
| │ │ └── mpz.h | |
| │ ├── object_serializer.h | |
| │ ├── optional.h | |
| │ ├── output_channel.h | |
| │ ├── pair.h | |
| │ ├── parser_exception.h | |
| │ ├── path.h | |
| │ ├── priority_queue.h | |
| │ ├── rb_map.h | |
| │ ├── rb_multi_map.h | |
| │ ├── rb_tree.h | |
| │ ├── rc.h | |
| │ ├── safe_arith.h | |
| │ ├── scoped_map.h | |
| │ ├── scoped_set.h | |
| │ ├── sequence.h | |
| │ ├── serializer.h | |
| │ ├── sexpr | |
| │ │ ├── format.h | |
| │ │ ├── init_module.h | |
| │ │ ├── option_declarations.h | |
| │ │ ├── options.h | |
| │ │ ├── sexpr_fn.h | |
| │ │ └── sexpr.h | |
| │ ├── shared_mutex.h | |
| │ ├── small_object_allocator.h | |
| │ ├── sstream.h | |
| │ ├── stackinfo.h | |
| │ ├── subscripted_name_set.h | |
| │ ├── task_builder.h | |
| │ ├── task.h | |
| │ ├── test.h | |
| │ ├── thread.h | |
| │ ├── timeit.h | |
| │ ├── timer.h | |
| │ ├── trie.h | |
| │ ├── unit.h | |
| │ ├── unlock_guard.h | |
| │ ├── utf8.h | |
| │ └── worker_queue.h | |
| └── lib | |
| └── lean | |
| ├── leanpkg | |
| │ ├── leanpkg | |
| │ │ ├── git.lean | |
| │ │ ├── lean_version.lean | |
| │ │ ├── main.lean | |
| │ │ ├── manifest.lean | |
| │ │ ├── proc.lean | |
| │ │ ├── resolve.lean | |
| │ │ └── toml.lean | |
| │ ├── leanpkg.toml | |
| │ └── README.md | |
| └── library | |
| ├── data | |
| │ ├── bitvec.lean | |
| │ ├── buffer | |
| │ │ └── parser.lean | |
| │ ├── buffer.lean | |
| │ ├── dlist.lean | |
| │ ├── lazy_list.lean | |
| │ ├── rbmap | |
| │ │ └── default.lean | |
| │ ├── rbtree | |
| │ │ ├── basic.lean | |
| │ │ ├── default.lean | |
| │ │ ├── find.lean | |
| │ │ ├── insert.lean | |
| │ │ ├── main.lean | |
| │ │ └── min_max.lean | |
| │ ├── stream.lean | |
| │ └── vector.lean | |
| ├── init | |
| │ ├── algebra | |
| │ │ ├── classes.lean | |
| │ │ ├── default.lean | |
| │ │ ├── functions.lean | |
| │ │ └── order.lean | |
| │ ├── cc_lemmas.lean | |
| │ ├── classical.lean | |
| │ ├── coe.lean | |
| │ ├── control | |
| │ │ ├── alternative.lean | |
| │ │ ├── applicative.lean | |
| │ │ ├── combinators.lean | |
| │ │ ├── default.lean | |
| │ │ ├── except.lean | |
| │ │ ├── functor.lean | |
| │ │ ├── id.lean | |
| │ │ ├── lawful.lean | |
| │ │ ├── lift.lean | |
| │ │ ├── monad_fail.lean | |
| │ │ ├── monad.lean | |
| │ │ ├── option.lean | |
| │ │ ├── reader.lean | |
| │ │ └── state.lean | |
| │ ├── core.lean | |
| │ ├── data | |
| │ │ ├── array | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── slice.lean | |
| │ │ ├── basic.lean | |
| │ │ ├── bool | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── lemmas.lean | |
| │ │ ├── char | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── classes.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── lemmas.lean | |
| │ │ ├── default.lean | |
| │ │ ├── fin | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── ops.lean | |
| │ │ ├── int | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── bitwise.lean | |
| │ │ │ ├── comp_lemmas.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── order.lean | |
| │ │ ├── list | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ ├── instances.lean | |
| │ │ │ ├── lemmas.lean | |
| │ │ │ └── qsort.lean | |
| │ │ ├── nat | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── bitwise.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ ├── div.lean | |
| │ │ │ ├── gcd.lean | |
| │ │ │ └── lemmas.lean | |
| │ │ ├── option | |
| │ │ │ ├── basic.lean | |
| │ │ │ └── instances.lean | |
| │ │ ├── ordering | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── lemmas.lean | |
| │ │ ├── prod.lean | |
| │ │ ├── punit.lean | |
| │ │ ├── quot.lean | |
| │ │ ├── rbmap | |
| │ │ │ ├── basic.lean | |
| │ │ │ └── default.lean | |
| │ │ ├── rbtree | |
| │ │ │ ├── basic.lean | |
| │ │ │ └── default.lean | |
| │ │ ├── repr.lean | |
| │ │ ├── set.lean | |
| │ │ ├── setoid.lean | |
| │ │ ├── sigma | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── lex.lean | |
| │ │ ├── string | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── ops.lean | |
| │ │ ├── subtype | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── instances.lean | |
| │ │ ├── sum | |
| │ │ │ ├── basic.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── instances.lean | |
| │ │ ├── to_string.lean | |
| │ │ └── unsigned | |
| │ │ ├── basic.lean | |
| │ │ ├── default.lean | |
| │ │ └── ops.lean | |
| │ ├── default.lean | |
| │ ├── function.lean | |
| │ ├── funext.lean | |
| │ ├── init.md | |
| │ ├── ite_simp.lean | |
| │ ├── logic.lean | |
| │ ├── meta | |
| │ │ ├── ac_tactics.lean | |
| │ │ ├── async_tactic.lean | |
| │ │ ├── attribute.lean | |
| │ │ ├── backward.lean | |
| │ │ ├── case_tag.lean | |
| │ │ ├── comp_value_tactics.lean | |
| │ │ ├── congr_lemma.lean | |
| │ │ ├── congr_tactic.lean | |
| │ │ ├── constructor_tactic.lean | |
| │ │ ├── contradiction_tactic.lean | |
| │ │ ├── converter | |
| │ │ │ ├── conv.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ └── interactive.lean | |
| │ │ ├── declaration.lean | |
| │ │ ├── decl_cmds.lean | |
| │ │ ├── default.lean | |
| │ │ ├── derive.lean | |
| │ │ ├── environment.lean | |
| │ │ ├── exceptional.lean | |
| │ │ ├── expr_address.lean | |
| │ │ ├── expr.lean | |
| │ │ ├── float.lean | |
| │ │ ├── format.lean | |
| │ │ ├── fun_info.lean | |
| │ │ ├── has_reflect.lean | |
| │ │ ├── hole_command.lean | |
| │ │ ├── injection_tactic.lean | |
| │ │ ├── interaction_monad.lean | |
| │ │ ├── interactive_base.lean | |
| │ │ ├── interactive.lean | |
| │ │ ├── lean | |
| │ │ │ └── parser.lean | |
| │ │ ├── level.lean | |
| │ │ ├── local_context.lean | |
| │ │ ├── match_tactic.lean | |
| │ │ ├── mk_dec_eq_instance.lean | |
| │ │ ├── mk_has_reflect_instance.lean | |
| │ │ ├── mk_has_sizeof_instance.lean | |
| │ │ ├── mk_inhabited_instance.lean | |
| │ │ ├── module_info.lean | |
| │ │ ├── name.lean | |
| │ │ ├── occurrences.lean | |
| │ │ ├── options.lean | |
| │ │ ├── pexpr.lean | |
| │ │ ├── rb_map.lean | |
| │ │ ├── rec_util.lean | |
| │ │ ├── ref.lean | |
| │ │ ├── relation_tactics.lean | |
| │ │ ├── rewrite_tactic.lean | |
| │ │ ├── set_get_option_tactics.lean | |
| │ │ ├── simp_tactic.lean | |
| │ │ ├── smt | |
| │ │ │ ├── congruence_closure.lean | |
| │ │ │ ├── default.lean | |
| │ │ │ ├── ematch.lean | |
| │ │ │ ├── interactive.lean | |
| │ │ │ ├── rsimp.lean | |
| │ │ │ └── smt_tactic.lean | |
| │ │ ├── tactic.lean | |
| │ │ ├── tagged_format.lean | |
| │ │ ├── task.lean | |
| │ │ ├── type_context.lean | |
| │ │ ├── vm.lean | |
| │ │ ├── well_founded_tactics.lean | |
| │ │ └── widget | |
| │ │ ├── basic.lean | |
| │ │ ├── default.lean | |
| │ │ ├── html_cmd.lean | |
| │ │ ├── interactive_expr.lean | |
| │ │ ├── replace_save_info.lean | |
| │ │ └── tactic_component.lean | |
| │ ├── propext.lean | |
| │ ├── util.lean | |
| │ ├── version.lean | |
| │ └── wf.lean | |
| ├── library.md | |
| ├── smt | |
| │ ├── arith.lean | |
| │ ├── array.lean | |
| │ ├── default.lean | |
| │ └── prove.lean | |
| ├── system | |
| │ ├── io_interface.lean | |
| │ ├── io.lean | |
| │ └── random.lean | |
| └── tools | |
| └── debugger | |
| ├── cli.lean | |
| ├── default.lean | |
| └── util.lean | |
| 151 directories, 585 files |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment