max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Joachim Breitner d16862fd33
feat: induction: allow complex arguments to motive in conclusion of eliminator (#8096) 
This PR lets `induction` accept eliminator where the motive application
in the conclusion has complex arguments; these are abstracted over using
`kabstract` if possible. This feature will go well with unfolding
induction principles (#8088).
2025-04-30 08:56:17 +00:00
..
Compiler fix: support borrowed params in the new compiler (#8127) 2025-04-28 17:02:47 +00:00
Data feat: NoZeroNatDivisors helper class for grind (#8111) 2025-04-26 15:14:27 +00:00
DocString feat: move non-essential metadata into .olean.server (#8068) 2025-04-24 08:12:26 +00:00
Elab feat: induction: allow complex arguments to motive in conclusion of eliminator (#8096) 2025-04-30 08:56:17 +00:00
Language chore: fix enabling module system (#8057) 2025-04-23 09:31:08 +00:00
Linter feat: deprecate Array.mkArray in favour of Array.replicate 2025-03-24 08:25:00 +01:00
Meta feat: induction: allow complex arguments to motive in conclusion of eliminator (#8096) 2025-04-30 08:56:17 +00:00
Parser fix: allow ascii <- in if let clauses (#8102) 2025-04-27 13:17:58 +00:00
ParserCompiler feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
PrettyPrinter fix: remove infinite loop in withFnRefWhenTagAppFns (#7904) 2025-04-10 17:16:29 +00:00
Server feat: do not export theorem bodies (#8090) 2025-04-25 20:22:32 +00:00
Util perf: no need to register axioms outside of the module system (#8121) 2025-04-26 16:14:00 +00:00
Widget fix: sorry in Infoview shouldn't show module name (#7813) 2025-04-10 21:47:07 +00:00
AddDecl.lean perf: no need to register axioms outside of the module system (#8121) 2025-04-26 16:14:00 +00:00
Attributes.lean feat: realizeConst for match equations (#7247) 2025-03-03 17:18:29 +00:00
AuxRecursor.lean refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794) 2025-04-02 16:19:12 +00:00
BuiltinDocAttr.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Class.lean chore: move MessageData.ofConstName earlier (#5877) 2024-10-29 21:23:51 +00:00
Compiler.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CoreM.lean doc: add docstrings to mkFreshUserName etc (#7947) 2025-04-14 04:17:45 +00:00
Data.lean chore: remove the old Lean.Data.HashMap implementation (#7519) 2025-03-20 23:49:55 +00:00
Declaration.lean feat: do not export theorem bodies (#8090) 2025-04-25 20:22:32 +00:00
DeclarationRange.lean feat: move non-essential metadata into .olean.server (#8068) 2025-04-24 08:12:26 +00:00
DocString.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
Elab.lean feat: #info_trees in command (#6964) 2025-02-06 03:11:53 +00:00
EnvExtension.lean feat: move non-essential metadata into .olean.server (#8068) 2025-04-24 08:12:26 +00:00
Environment.lean chore: fix default of Import.isExported 2025-04-29 10:58:27 +02:00
Exception.lean feat: 'unknown identifier' code actions (#7665) 2025-04-02 09:43:40 +00:00
Expr.lean fix: grind +splitImp, arrow propagator, missing normalization rule (#8158) 2025-04-28 22:59:43 +00:00
HeadIndex.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
Hygiene.lean chore: remove the coercion from String to Name (#3589) 2024-03-21 23:46:03 +00:00
ImportingFlag.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InternalExceptionId.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
KeyedDeclsAttribute.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LabelAttribute.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
Level.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
Linter.lean chore: fix variable names in List lemmas (#6953) 2025-02-05 09:49:14 +00:00
LoadDynlib.lean feat: smarter plugin loading (#7090) 2025-02-18 23:03:52 +00:00
LocalContext.lean fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075) 2025-03-03 16:10:54 +00:00
Log.lean feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366) 2025-03-07 13:50:56 +00:00
Message.lean chore: avoid unnecessary quotations in cutsat traces and counterexamples (#7877) 2025-04-08 21:01:07 +00:00
Meta.lean feat: binderNameHint (#6947) 2025-02-06 11:03:27 +00:00
MetavarContext.lean doc: fix typo in MetavarDecl docstring (#8069) 2025-04-23 22:00:13 +00:00
Modifiers.lean refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794) 2025-04-02 16:19:12 +00:00
MonadEnv.lean chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00
Namespace.lean refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794) 2025-04-02 16:19:12 +00:00
Parser.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
ParserCompiler.lean feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800) 2025-01-28 23:34:30 +00:00
PremiseSelection.lean feat: premise selection API (#7061) 2025-02-14 04:08:18 +00:00
PrettyPrinter.lean fix: don't reset localInstances in delaboration (#8022) 2025-04-19 15:39:16 +00:00
PrivateName.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
ProjFns.lean refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794) 2025-04-02 16:19:12 +00:00
ReducibilityAttrs.lean feat: add async support to more extensions and constructions (#7363) 2025-03-06 14:27:45 +00:00
Replay.lean chore: Mathlib fixes (#7327) 2025-03-04 13:41:30 +00:00
ReservedNameAction.lean feat: elaborate theorem bodies in parallel (#7084) 2025-03-14 07:50:42 +00:00
ResolveName.lean perf: use isReservedName in Environment.findAsync? 2025-03-25 17:22:22 +01:00
Runtime.lean feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
ScopedEnvExtension.lean feat: make more constructions async-compatible (#7384) 2025-03-10 09:56:30 +00:00
Server.lean fix: do not cancel async elaboration tasks (#7175) 2025-02-21 17:24:36 +00:00
Structure.lean refactor: factor out common code for structure default values (#7737) 2025-03-31 22:40:39 +00:00
SubExpr.lean chore: cleanup imports (#5825) 2024-10-23 23:51:13 +00:00
Syntax.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
ToExpr.lean feat: ToExpr IntX (#7268) 2025-02-28 09:32:30 +00:00
ToLevel.lean feat: upstream ToLevel from mathlib (#6285) 2024-12-05 05:50:32 +00:00
Util.lean feat: simp +arith sorts linear atoms (#7040) 2025-02-11 23:37:30 +00:00
Widget.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00