Files

 master

/

kernel

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

nomeata

and

leodemoura

fix: bv_omega to use -implicitDefEqProofs (leanprover#7387)

Mar 9, 2025

dd91d7e · Mar 9, 2025

History

History

This branch is 21 commits behind leanprover/lean4:master.

/

kernel

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
CMakeLists.txt		CMakeLists.txt	perf: add lean_instantiate_level_mvars (leanprover#4910)	Aug 4, 2024
abstract.cpp		abstract.cpp	feat: generalize Expr.abstractRange	Mar 9, 2022
abstract.h		abstract.h	chore: remove Expr.localE constructor	Nov 1, 2020
declaration.cpp		declaration.cpp	fix: RecursorVal.getInduct to return name of major argument’s type (l…	Oct 21, 2024
declaration.h		declaration.h	fix: RecursorVal.getInduct to return name of major argument’s type (l…	Oct 21, 2024
environment.cpp		environment.cpp	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
environment.h		environment.h	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
equiv_manager.cpp		equiv_manager.cpp	chore: reduce src/include/lean	Sep 7, 2021
equiv_manager.h		equiv_manager.h	chore(*): rename expr_struct_* to expr_*	Apr 9, 2018
expr.cpp		expr.cpp	perf: has_univ_mvar, has_univ_mvar, and has_fvar in C++ (leanpr…	Oct 21, 2024
expr.h		expr.h	perf: optimize sorry detection in unused variables linter (leanprov…	Feb 22, 2025
expr_cache.cpp		expr_cache.cpp	refactor(kernel/expr): implement expr using runtime/object	Jun 21, 2018
expr_cache.h		expr_cache.h	refactor(kernel): add expr_cache	Feb 3, 2015
expr_eq_fn.cpp		expr_eq_fn.cpp	chore: fix typo in hash code for Expr equality test (leanprover#4990)	Aug 12, 2024
expr_eq_fn.h		expr_eq_fn.h	feat(library/type_context): allow us to control whether binder inform…	Aug 1, 2016
expr_maps.h		expr_maps.h	chore(*): rename expr_struct_* to expr_*	Apr 9, 2018
expr_sets.h		expr_sets.h	chore: reduce src/include/lean	Sep 7, 2021
find_fn.h		find_fn.h	refactor(kernel/find_fn): simplify find_fn module	Jul 24, 2014
for_each_fn.cpp		for_each_fn.cpp	perf: optimize sorry detection in unused variables linter (leanprov…	Feb 22, 2025
for_each_fn.h		for_each_fn.h	perf: for_each with precise cache (leanprover#4794)	Jul 20, 2024
inductive.cpp		inductive.cpp	refactor: InductiveVal.numNested instead of .isNested	Jul 8, 2024
inductive.h		inductive.h	fix: RecursorVal.getInduct to return name of major argument’s type (l…	Oct 21, 2024
init_module.cpp		init_module.cpp	fix: Windows needs more LEAN_EXPORTs	Aug 12, 2024
init_module.h		init_module.h	fix: Windows needs more LEAN_EXPORTs	Aug 12, 2024
instantiate.cpp		instantiate.cpp	perf: instantiateExprMVars (leanprover#4915)	Aug 5, 2024
instantiate.h		instantiate.h	perf: instantiateExprMVars (leanprover#4915)	Aug 5, 2024
instantiate_mvars.cpp		instantiate_mvars.cpp	chore: fix spelling mistakes in non-Lean files (leanprover#5430)	Sep 23, 2024
kernel_exception.h		kernel_exception.h	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
level.cpp		level.cpp	chore: remove remnants of C++ format	Nov 18, 2022
level.h		level.h	perf: add lean_instantiate_level_mvars (leanprover#4910)	Aug 4, 2024
local_ctx.cpp		local_ctx.cpp	chore: reduce src/include/lean	Sep 7, 2021
local_ctx.h		local_ctx.h	perf: fix implementation of move constructors and move assignment ope… (	Aug 2, 2024
quot.cpp		quot.cpp	fix: binder name	Aug 26, 2021
quot.h		quot.h	fix: quot reduction bug	Oct 12, 2023
replace_fn.cpp		replace_fn.cpp	perf: optimize sorry detection in unused variables linter (leanprov…	Feb 22, 2025
replace_fn.h		replace_fn.h	chore: reduce src/include/lean	Sep 7, 2021
trace.cpp		trace.cpp	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
trace.h		trace.h	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
type_checker.cpp		type_checker.cpp	fix: bv_omega to use -implicitDefEqProofs (leanprover#7387)	Mar 9, 2025
type_checker.h		type_checker.h	feat: split Lean.Kernel.Environment from Lean.Environment (leanpr…	Jan 18, 2025
View all files