Created
June 14, 2020 19:32
-
-
Save r-ryantm/8ad5cb81115cb612e686c1bac20d83ee 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/qhbycb66zz7qzk4x9klpwdsclf6d2f3j-lean-3.16.2 | |
├── bin | |
│ ├── lean | |
│ ├── leanchecker | |
│ └── leanpkg | |
├── include | |
│ ├── lean_bool.h | |
│ ├── lean_decl.h | |
│ ├── lean_env.h | |
│ ├── lean_exception.h | |
│ ├── lean_expr.h | |
│ ├── lean_ext | |
│ │ ├── api | |
│ │ │ ├── decl.h | |
│ │ │ ├── exception.h | |
│ │ │ ├── expr.h | |
│ │ │ ├── inductive.h | |
│ │ │ ├── ios.h | |
│ │ │ ├── lean_bool.h | |
│ │ │ ├── lean_decl.h | |
│ │ │ ├── lean_env.h | |
│ │ │ ├── lean_exception.h | |
│ │ │ ├── lean_expr.h | |
│ │ │ ├── lean.h | |
│ │ │ ├── lean_inductive.h | |
│ │ │ ├── lean_ios.h | |
│ │ │ ├── lean_macros.h | |
│ │ │ ├── lean_module.h | |
│ │ │ ├── lean_name.h | |
│ │ │ ├── lean_options.h | |
│ │ │ ├── lean_parser.h | |
│ │ │ ├── lean_string.h | |
│ │ │ ├── lean_type_checker.h | |
│ │ │ ├── lean_univ.h | |
│ │ │ ├── name.h | |
│ │ │ ├── options.h | |
│ │ │ ├── string.h | |
│ │ │ ├── type_checker.h | |
│ │ │ └── univ.h | |
│ │ ├── build | |
│ │ │ ├── api | |
│ │ │ │ └── CMakeFiles | |
│ │ │ │ └── api.dir | |
│ │ │ ├── checker | |
│ │ │ │ └── CMakeFiles | |
│ │ │ │ └── leanchecker.dir | |
│ │ │ ├── CMakeFiles | |
│ │ │ │ ├── 3.17.2 | |
│ │ │ │ │ ├── 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 | |
│ │ │ ├── register_module.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 | |
│ │ │ ├── shared | |
│ │ │ ├── shell | |
│ │ │ └── util | |
│ │ │ ├── interval | |
│ │ │ │ └── check.h | |
│ │ │ └── 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 | |
│ │ │ ├── double.h | |
│ │ │ ├── float.h | |
│ │ │ ├── gcd.h | |
│ │ │ ├── init_module.h | |
│ │ │ ├── mpbq.h | |
│ │ │ ├── mpq.h | |
│ │ │ ├── mpz.h | |
│ │ │ ├── numeric_traits.h | |
│ │ │ ├── power.h | |
│ │ │ ├── primes.h | |
│ │ │ ├── register_module.h | |
│ │ │ ├── remainder.h | |
│ │ │ ├── xnumeral.h | |
│ │ │ └── zpz.h | |
│ │ ├── object_serializer.h | |
│ │ ├── optional.h | |
│ │ ├── output_channel.h | |
│ │ ├── pair.h | |
│ │ ├── parser_exception.h | |
│ │ ├── path.h | |
│ │ ├── polynomial | |
│ │ │ └── polynomial.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 | |
│ │ │ ├── register_module.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 | |
│ ├── lean.h | |
│ ├── lean_inductive.h | |
│ ├── lean_ios.h | |
│ ├── lean_macros.h | |
│ ├── lean_module.h | |
│ ├── lean_name.h | |
│ ├── lean_options.h | |
│ ├── lean_parser.h | |
│ ├── lean_string.h | |
│ ├── lean_type_checker.h | |
│ └── lean_univ.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 | |
158 directories, 643 files |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment