Created
November 11, 2020 11:58
-
-
Save r-ryantm/ee1e102c80db45aa0221969901e38790 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/7brd4rakl3a62fhp41fs7sxvfdsgz7y2-lean-3.23.0 | |
├── bin | |
│ ├── lean | |
│ ├── leanchecker | |
│ └── leanpkg | |
├── include | |
│ └── lean_ext | |
│ ├── 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_json.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 | |
│ │ ├── 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 | |
│ │ ├── git.olean | |
│ │ ├── lean_version.lean | |
│ │ ├── lean_version.olean | |
│ │ ├── main.lean | |
│ │ ├── main.olean | |
│ │ ├── manifest.lean | |
│ │ ├── manifest.olean | |
│ │ ├── proc.lean | |
│ │ ├── proc.olean | |
│ │ ├── resolve.lean | |
│ │ ├── resolve.olean | |
│ │ ├── toml.lean | |
│ │ └── toml.olean | |
│ ├── leanpkg.toml | |
│ └── README.md | |
└── library | |
├── data | |
│ ├── buffer | |
│ │ ├── parser.lean | |
│ │ └── parser.olean | |
│ ├── buffer.lean | |
│ ├── buffer.olean | |
│ ├── dlist.lean | |
│ ├── dlist.olean | |
│ ├── lazy_list.lean | |
│ ├── lazy_list.olean | |
│ ├── rbmap | |
│ │ ├── default.lean | |
│ │ └── default.olean | |
│ ├── rbtree | |
│ │ ├── basic.lean | |
│ │ ├── basic.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── find.lean | |
│ │ ├── find.olean | |
│ │ ├── insert.lean | |
│ │ ├── insert.olean | |
│ │ ├── main.lean | |
│ │ ├── main.olean | |
│ │ ├── min_max.lean | |
│ │ └── min_max.olean | |
│ ├── stream.lean | |
│ ├── stream.olean | |
│ ├── vector.lean | |
│ └── vector.olean | |
├── init | |
│ ├── algebra | |
│ │ ├── classes.lean | |
│ │ ├── classes.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── functions.lean | |
│ │ ├── functions.olean | |
│ │ ├── order.lean | |
│ │ └── order.olean | |
│ ├── cc_lemmas.lean | |
│ ├── cc_lemmas.olean | |
│ ├── classical.lean | |
│ ├── classical.olean | |
│ ├── coe.lean | |
│ ├── coe.olean | |
│ ├── control | |
│ │ ├── alternative.lean | |
│ │ ├── alternative.olean | |
│ │ ├── applicative.lean | |
│ │ ├── applicative.olean | |
│ │ ├── combinators.lean | |
│ │ ├── combinators.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── except.lean | |
│ │ ├── except.olean | |
│ │ ├── functor.lean | |
│ │ ├── functor.olean | |
│ │ ├── id.lean | |
│ │ ├── id.olean | |
│ │ ├── lawful.lean | |
│ │ ├── lawful.olean | |
│ │ ├── lift.lean | |
│ │ ├── lift.olean | |
│ │ ├── monad_fail.lean | |
│ │ ├── monad_fail.olean | |
│ │ ├── monad.lean | |
│ │ ├── monad.olean | |
│ │ ├── option.lean | |
│ │ ├── option.olean | |
│ │ ├── reader.lean | |
│ │ ├── reader.olean | |
│ │ ├── state.lean | |
│ │ └── state.olean | |
│ ├── core.lean | |
│ ├── core.olean | |
│ ├── data | |
│ │ ├── array | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── slice.lean | |
│ │ │ └── slice.olean | |
│ │ ├── basic.lean | |
│ │ ├── basic.olean | |
│ │ ├── bool | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── lemmas.lean | |
│ │ │ └── lemmas.olean | |
│ │ ├── char | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── classes.lean | |
│ │ │ ├── classes.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── lemmas.lean | |
│ │ │ └── lemmas.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── fin | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── ops.lean | |
│ │ │ └── ops.olean | |
│ │ ├── int | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── bitwise.lean | |
│ │ │ ├── bitwise.olean | |
│ │ │ ├── comp_lemmas.lean | |
│ │ │ ├── comp_lemmas.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── order.lean | |
│ │ │ └── order.olean | |
│ │ ├── list | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── instances.lean | |
│ │ │ ├── instances.olean | |
│ │ │ ├── lemmas.lean | |
│ │ │ ├── lemmas.olean | |
│ │ │ ├── qsort.lean | |
│ │ │ └── qsort.olean | |
│ │ ├── nat | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── bitwise.lean | |
│ │ │ ├── bitwise.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── div.lean | |
│ │ │ ├── div.olean | |
│ │ │ ├── gcd.lean | |
│ │ │ ├── gcd.olean | |
│ │ │ ├── lemmas.lean | |
│ │ │ └── lemmas.olean | |
│ │ ├── option | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── instances.lean | |
│ │ │ └── instances.olean | |
│ │ ├── ordering | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── lemmas.lean | |
│ │ │ └── lemmas.olean | |
│ │ ├── prod.lean | |
│ │ ├── prod.olean | |
│ │ ├── punit.lean | |
│ │ ├── punit.olean | |
│ │ ├── quot.lean | |
│ │ ├── quot.olean | |
│ │ ├── rbmap | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ └── default.olean | |
│ │ ├── rbtree | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ └── default.olean | |
│ │ ├── repr.lean | |
│ │ ├── repr.olean | |
│ │ ├── set.lean | |
│ │ ├── setoid.lean | |
│ │ ├── setoid.olean | |
│ │ ├── set.olean | |
│ │ ├── sigma | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── lex.lean | |
│ │ │ └── lex.olean | |
│ │ ├── string | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── ops.lean | |
│ │ │ └── ops.olean | |
│ │ ├── subtype | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── instances.lean | |
│ │ │ └── instances.olean | |
│ │ ├── sum | |
│ │ │ ├── basic.lean | |
│ │ │ ├── basic.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── instances.lean | |
│ │ │ └── instances.olean | |
│ │ ├── to_string.lean | |
│ │ ├── to_string.olean | |
│ │ └── unsigned | |
│ │ ├── basic.lean | |
│ │ ├── basic.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── ops.lean | |
│ │ └── ops.olean | |
│ ├── default.lean | |
│ ├── default.olean | |
│ ├── function.lean | |
│ ├── function.olean | |
│ ├── funext.lean | |
│ ├── funext.olean | |
│ ├── init.md | |
│ ├── ite_simp.lean | |
│ ├── ite_simp.olean | |
│ ├── logic.lean | |
│ ├── logic.olean | |
│ ├── meta | |
│ │ ├── ac_tactics.lean | |
│ │ ├── ac_tactics.olean | |
│ │ ├── async_tactic.lean | |
│ │ ├── async_tactic.olean | |
│ │ ├── attribute.lean | |
│ │ ├── attribute.olean | |
│ │ ├── backward.lean | |
│ │ ├── backward.olean | |
│ │ ├── case_tag.lean | |
│ │ ├── case_tag.olean | |
│ │ ├── comp_value_tactics.lean | |
│ │ ├── comp_value_tactics.olean | |
│ │ ├── congr_lemma.lean | |
│ │ ├── congr_lemma.olean | |
│ │ ├── congr_tactic.lean | |
│ │ ├── congr_tactic.olean | |
│ │ ├── constructor_tactic.lean | |
│ │ ├── constructor_tactic.olean | |
│ │ ├── contradiction_tactic.lean | |
│ │ ├── contradiction_tactic.olean | |
│ │ ├── converter | |
│ │ │ ├── conv.lean | |
│ │ │ ├── conv.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── interactive.lean | |
│ │ │ └── interactive.olean | |
│ │ ├── declaration.lean | |
│ │ ├── declaration.olean | |
│ │ ├── decl_cmds.lean | |
│ │ ├── decl_cmds.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── derive.lean | |
│ │ ├── derive.olean | |
│ │ ├── environment.lean | |
│ │ ├── environment.olean | |
│ │ ├── exceptional.lean | |
│ │ ├── exceptional.olean | |
│ │ ├── expr_address.lean | |
│ │ ├── expr_address.olean | |
│ │ ├── expr.lean | |
│ │ ├── expr.olean | |
│ │ ├── float.lean | |
│ │ ├── float.olean | |
│ │ ├── format.lean | |
│ │ ├── format.olean | |
│ │ ├── fun_info.lean | |
│ │ ├── fun_info.olean | |
│ │ ├── has_reflect.lean | |
│ │ ├── has_reflect.olean | |
│ │ ├── hole_command.lean | |
│ │ ├── hole_command.olean | |
│ │ ├── injection_tactic.lean | |
│ │ ├── injection_tactic.olean | |
│ │ ├── interaction_monad.lean | |
│ │ ├── interaction_monad.olean | |
│ │ ├── interactive_base.lean | |
│ │ ├── interactive_base.olean | |
│ │ ├── interactive.lean | |
│ │ ├── interactive.olean | |
│ │ ├── json.lean | |
│ │ ├── json.olean | |
│ │ ├── lean | |
│ │ │ ├── parser.lean | |
│ │ │ └── parser.olean | |
│ │ ├── level.lean | |
│ │ ├── level.olean | |
│ │ ├── local_context.lean | |
│ │ ├── local_context.olean | |
│ │ ├── match_tactic.lean | |
│ │ ├── match_tactic.olean | |
│ │ ├── mk_dec_eq_instance.lean | |
│ │ ├── mk_dec_eq_instance.olean | |
│ │ ├── mk_has_reflect_instance.lean | |
│ │ ├── mk_has_reflect_instance.olean | |
│ │ ├── mk_has_sizeof_instance.lean | |
│ │ ├── mk_has_sizeof_instance.olean | |
│ │ ├── mk_inhabited_instance.lean | |
│ │ ├── mk_inhabited_instance.olean | |
│ │ ├── module_info.lean | |
│ │ ├── module_info.olean | |
│ │ ├── name.lean | |
│ │ ├── name.olean | |
│ │ ├── occurrences.lean | |
│ │ ├── occurrences.olean | |
│ │ ├── options.lean | |
│ │ ├── options.olean | |
│ │ ├── pexpr.lean | |
│ │ ├── pexpr.olean | |
│ │ ├── rb_map.lean | |
│ │ ├── rb_map.olean | |
│ │ ├── rec_util.lean | |
│ │ ├── rec_util.olean | |
│ │ ├── ref.lean | |
│ │ ├── ref.olean | |
│ │ ├── relation_tactics.lean | |
│ │ ├── relation_tactics.olean | |
│ │ ├── rewrite_tactic.lean | |
│ │ ├── rewrite_tactic.olean | |
│ │ ├── set_get_option_tactics.lean | |
│ │ ├── set_get_option_tactics.olean | |
│ │ ├── simp_tactic.lean | |
│ │ ├── simp_tactic.olean | |
│ │ ├── smt | |
│ │ │ ├── congruence_closure.lean | |
│ │ │ ├── congruence_closure.olean | |
│ │ │ ├── default.lean | |
│ │ │ ├── default.olean | |
│ │ │ ├── ematch.lean | |
│ │ │ ├── ematch.olean | |
│ │ │ ├── interactive.lean | |
│ │ │ ├── interactive.olean | |
│ │ │ ├── rsimp.lean | |
│ │ │ ├── rsimp.olean | |
│ │ │ ├── smt_tactic.lean | |
│ │ │ └── smt_tactic.olean | |
│ │ ├── tactic.lean | |
│ │ ├── tactic.olean | |
│ │ ├── tagged_format.lean | |
│ │ ├── tagged_format.olean | |
│ │ ├── task.lean | |
│ │ ├── task.olean | |
│ │ ├── type_context.lean | |
│ │ ├── type_context.olean | |
│ │ ├── vm.lean | |
│ │ ├── vm.olean | |
│ │ ├── well_founded_tactics.lean | |
│ │ ├── well_founded_tactics.olean | |
│ │ └── widget | |
│ │ ├── basic.lean | |
│ │ ├── basic.olean | |
│ │ ├── default.lean | |
│ │ ├── default.olean | |
│ │ ├── html_cmd.lean | |
│ │ ├── html_cmd.olean | |
│ │ ├── interactive_expr.lean | |
│ │ ├── interactive_expr.olean | |
│ │ ├── replace_save_info.lean | |
│ │ ├── replace_save_info.olean | |
│ │ ├── tactic_component.lean | |
│ │ └── tactic_component.olean | |
│ ├── propext.lean | |
│ ├── propext.olean | |
│ ├── util.lean | |
│ ├── util.olean | |
│ ├── version.lean | |
│ ├── version.olean | |
│ ├── wf.lean | |
│ └── wf.olean | |
├── library.md | |
├── smt | |
│ ├── arith.lean | |
│ ├── arith.olean | |
│ ├── array.lean | |
│ ├── array.olean | |
│ ├── default.lean | |
│ ├── default.olean | |
│ ├── prove.lean | |
│ └── prove.olean | |
├── system | |
│ ├── io_interface.lean | |
│ ├── io_interface.olean | |
│ ├── io.lean | |
│ ├── io.olean | |
│ ├── random.lean | |
│ └── random.olean | |
└── tools | |
└── debugger | |
├── cli.lean | |
├── cli.olean | |
├── default.lean | |
├── default.olean | |
├── util.lean | |
└── util.olean | |
74 directories, 775 files |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment