max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/stage0/stdlib/Init
History
Leonardo de Moura d963d33985
feat: add grind_pattern constraints (#11187) 
This PR adds syntax for specifying `grind_pattern` constraints and
extends the `EMatchTheorem` object.

--- 
Note: We need a manual stage0 update because it affects the .olean
files.
2025-11-14 18:27:17 -08:00
..
Control chore: update stage0 2025-11-13 02:05:09 +00:00
Data feat: add grind_pattern constraints (#11187) 2025-11-14 18:27:17 -08:00
Grind feat: add grind_pattern constraints (#11187) 2025-11-14 18:27:17 -08:00
GrindInstances chore: update stage0 2025-10-28 13:47:28 +00:00
Internal chore: update stage0 2025-10-25 11:32:01 +00:00
Meta chore: update stage0 2025-11-13 02:05:09 +00:00
Omega chore: update stage0 2025-11-13 02:05:09 +00:00
System chore: update stage0 2025-11-13 02:05:09 +00:00
BinderNameHint.c chore: update stage0 2025-10-23 08:03:18 +00:00
BinderPredicates.c chore: update stage0 2025-10-25 11:32:01 +00:00
ByCases.c chore: update stage0 2025-10-25 11:32:01 +00:00
Classical.c chore: update stage0 2025-10-23 08:03:18 +00:00
Coe.c chore: update stage0 2025-10-23 08:03:18 +00:00
Control.c chore: update stage0 2025-10-23 08:03:18 +00:00
Conv.c chore: update stage0 2025-10-25 11:32:01 +00:00
Core.c chore: update stage0 2025-10-30 07:41:23 +00:00
Data.c chore: update stage0 2025-10-25 11:32:01 +00:00
Dynamic.c chore: update stage0 2025-10-23 08:03:18 +00:00
Ext.c chore: update stage0 2025-10-25 11:32:01 +00:00
GetElem.c chore: update stage0 2025-11-13 02:05:09 +00:00
Grind.c chore: update stage0 2025-11-13 02:05:09 +00:00
GrindInstances.c chore: update stage0 2025-10-23 08:03:18 +00:00
Guard.c chore: update stage0 2025-10-23 08:03:18 +00:00
Hints.c chore: update stage0 2025-10-23 08:03:18 +00:00
Internal.c chore: update stage0 2025-10-23 08:03:18 +00:00
LawfulBEqTactics.c chore: update stage0 2025-10-23 08:03:18 +00:00
MacroTrace.c chore: update stage0 2025-10-25 11:32:01 +00:00
Meta.c chore: update stage0 2025-11-13 02:05:09 +00:00
MetaTypes.c chore: update stage0 2025-11-03 23:26:40 +11:00
MethodSpecsSimp.c chore: update stage0 2025-10-23 08:03:18 +00:00
Notation.c chore: update stage0 2025-11-03 02:54:49 +00:00
NotationExtra.c chore: update stage0 2025-11-13 02:05:09 +00:00
Omega.c chore: update stage0 2025-10-23 08:03:18 +00:00
Prelude.c chore: update stage0 2025-11-03 02:54:49 +00:00
PropLemmas.c chore: update stage0 2025-10-30 07:41:23 +00:00
RCases.c chore: update stage0 2025-10-23 08:03:18 +00:00
ShareCommon.c chore: update stage0 2025-10-23 08:03:18 +00:00
SimpLemmas.c chore: update stage0 2025-10-23 08:03:18 +00:00
Simproc.c chore: update stage0 2025-11-13 02:05:09 +00:00
SizeOf.c chore: update stage0 2025-10-23 08:03:18 +00:00
SizeOfLemmas.c chore: update stage0 2025-10-23 08:03:18 +00:00
Syntax.c chore: update stage0 2025-10-23 08:03:18 +00:00
System.c chore: update stage0 2025-10-23 08:03:18 +00:00
Tactics.c chore: update stage0 2025-11-13 02:05:09 +00:00
TacticsExtra.c chore: update stage0 2025-11-13 02:05:09 +00:00
Task.c chore: update stage0 2025-11-13 02:05:09 +00:00
Try.c feat: add grind_pattern constraints (#11187) 2025-11-14 18:27:17 -08:00
Util.c chore: update stage0 2025-11-13 02:05:09 +00:00
WF.c chore: update stage0 2025-10-23 08:03:18 +00:00
WFTactics.c chore: update stage0 2025-10-25 11:32:01 +00:00
While.c chore: update stage0 2025-10-25 11:32:01 +00:00