max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg
History
Joachim Breitner f20cae3729
fix: no defeq equations for irreducible definitions (#12429) 
This PR sets the `irreducible` attribute before generating the equations
for recursive definitions. This prevents these equations to be marked as
`defeq`, which could lead to `simp` generation proofs that do not type
check at default transparency.

This issue is surfacing more easily since well-founded recursion on
`Nat` is implemented with a dedicated fix point operator (#7965). Before
that, `WellFounded.fix` was used, which is inherently not reducing, so
we did get the desired result even without the explicit reducibility
setting.

Fixes #12398.
2026-02-11 11:49:10 +00:00
..
builtin_attr chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
cbv_attr feat: add cbv_eval attribute (#12296) 2026-02-10 15:41:42 +00:00
debug chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
def_clash chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
deriving chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
frontend chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
initialize fix: run @[init] declarations in declaration order (#12221) 2026-01-29 15:32:56 +00:00
leanchecker feat: one axiom per native computation (#12217) 2026-02-03 10:15:01 +00:00
linter_set chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
misc fix: local syntax should create private definitions 2025-08-19 14:49:12 -07:00
mod_clash chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
module fix: no defeq equations for irreducible definitions (#12429) 2026-02-11 11:49:10 +00:00
path with spaces chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
prv feat: improve error message in the case of type class synthesis failure (#11245) 2025-11-21 21:24:27 +00:00
rebuild feat: module system is no longer experimental (#11637) 2025-12-12 21:20:26 +00:00
setup chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
signal chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
structure_docstrings chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
test_extern chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_attr feat: shake: track simpset/grindset uses (#12375) 2026-02-07 15:19:15 +00:00
user_attr_app chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_ext chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_opt chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_plugin chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
ver_clash test: more .git cleanup (#12238) 2026-01-29 17:43:31 +00:00
.gitignore test: module clash across packages (#11246) 2025-11-19 02:23:34 +00:00