| .. |
|
AC
|
|
|
|
Grind
|
test: cutsat cooper resolution (#7354)
|
2025-03-06 00:40:38 +00:00 |
|
Simp
|
feat: IntX simprocs (#7228)
|
2025-03-03 13:37:57 +00:00 |
|
Try
|
feat: try? to use fun_induction (#7082)
|
2025-02-18 16:06:58 +00:00 |
|
AC.lean
|
|
|
|
Acyclic.lean
|
|
|
|
Apply.lean
|
feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)
|
2024-11-22 03:05:51 +00:00 |
|
Assert.lean
|
|
|
|
Assumption.lean
|
|
|
|
AuxLemma.lean
|
|
|
|
Backtrack.lean
|
|
|
|
Cases.lean
|
feat: split on match-expressions in the grind tactic (#6569)
|
2025-01-08 03:10:11 +00:00 |
|
Cleanup.lean
|
|
|
|
Clear.lean
|
feat: Array.insertIdx/eraseIdx take a tactic-provided proof (#6133)
|
2024-11-20 09:52:38 +00:00 |
|
Congr.lean
|
|
|
|
Constructor.lean
|
|
|
|
Contradiction.lean
|
feat: close goals using match-expression conditions in grind (#6783)
|
2025-01-26 17:13:11 +00:00 |
|
Delta.lean
|
|
|
|
ElimInfo.lean
|
feat: induction tactic to err on extra targets (#7224)
|
2025-02-25 20:53:16 +00:00 |
|
ExposeNames.lean
|
fix: prevent exact? and apply? from suggesting invalid tactics (#7192)
|
2025-02-25 15:24:09 +00:00 |
|
Ext.lean
|
refactor: move ext environment extension to Lean.Meta.Tactic
|
2025-01-17 12:31:14 -08:00 |
|
FunInd.lean
|
feat: identify more fixed parameters (#7166)
|
2025-03-04 22:26:20 +00:00 |
|
FunIndCollect.lean
|
feat: try? to use fun_induction (#7082)
|
2025-02-18 16:06:58 +00:00 |
|
FunIndInfo.lean
|
feat: identify more fixed parameters (#7166)
|
2025-03-04 22:26:20 +00:00 |
|
FVarSubst.lean
|
feat: offset constraints support for the grind tactic (#6603)
|
2025-01-12 20:38:39 +00:00 |
|
Generalize.lean
|
|
|
|
Grind.lean
|
feat: add Grind.mkDiseqProof? (#7231)
|
2025-02-25 23:40:07 +00:00 |
|
IndependentOf.lean
|
|
|
|
Induction.lean
|
feat: cleanup of get and back functions on List/Array (#7059)
|
2025-02-17 01:43:45 +00:00 |
|
Injection.lean
|
fix: nontermination while generating equation lemmas for match-expressions (#6180)
|
2024-11-23 00:06:34 +00:00 |
|
Intro.lean
|
|
|
|
LibrarySearch.lean
|
feat: try? tactic (#6905)
|
2025-02-02 06:37:49 +00:00 |
|
NormCast.lean
|
|
|
|
Refl.lean
|
|
|
|
Rename.lean
|
|
|
|
Repeat.lean
|
|
|
|
Replace.lean
|
fix: use Expr.equal instead of == in MVarId.replaceTargetDefEq and MVarId.replaceLocalDeclDefEq (#6098)
|
2024-11-16 02:03:16 +00:00 |
|
Revert.lean
|
fix: revert creates natural metavariable goal (#6145)
|
2024-11-21 23:00:57 +00:00 |
|
Rewrite.lean
|
feat: binderNameHint (#6947)
|
2025-02-06 11:03:27 +00:00 |
|
Rewrites.lean
|
|
|
|
Rfl.lean
|
fix: isDefEq, whnf, simp caching and configuration (#6053)
|
2024-11-18 01:17:26 +00:00 |
|
Simp.lean
|
feat: cutsat preparations (#7097)
|
2025-02-16 02:52:14 +00:00 |
|
SolveByElim.lean
|
|
|
|
Split.lean
|
refactor: simpMatch to not etaStruct (#6901)
|
2025-02-01 19:04:05 +00:00 |
|
SplitIf.lean
|
feat: partial_fixpoint: partial functions with equations (#6355)
|
2025-01-21 09:54:30 +00:00 |
|
Subst.lean
|
feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)
|
2024-11-22 03:05:51 +00:00 |
|
Symm.lean
|
fix: isDefEq, whnf, simp caching and configuration (#6053)
|
2024-11-18 01:17:26 +00:00 |
|
Try.lean
|
feat: improve try? suggestion (#6991)
|
2025-02-07 16:33:25 +00:00 |
|
TryThis.lean
|
fix: missing indents in Try this message (#7191)
|
2025-02-25 16:55:50 +00:00 |
|
Unfold.lean
|
|
|
|
UnifyEq.lean
|
|
|
|
Util.lean
|
feat: labeled and unique sorries (#5757)
|
2024-12-11 23:53:02 +00:00 |
