lean4-htt

History

Kyle Miller b6a0d63612 feat: have "motive is not type correct" come with an explanation (#6168 ) This PR extends the "motive is not type correct" error message for the rewrite tactic to explain what it means. It also pretty prints the type-incorrect motive and reports the type error. Suggested [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/tactic.20'rewrite'.20failed.2C.20motive.20is.20not.20type.20correct/near/483545154).		2024-11-22 23:56:17 +00:00
..
Compiler	feat: `Nat.(fold\|foldRev\|any\|all)M?` take a function which sees the upper bound (#6139 )	2024-11-22 03:05:51 +00:00
Data	feat: `Nat.(fold\|foldRev\|any\|all)M?` take a function which sees the upper bound (#6139 )	2024-11-22 03:05:51 +00:00
DocString	fix: Lake: brittle dependency on env ext name	2024-10-07 13:26:07 +02:00
Elab	chore: refactor Elab.StructInst to use `mutual` for its `structure`s/`inductive`s (#6174 )	2024-11-22 19:17:48 +00:00
Language	feat: creation and reporting for asynchronous elaboration tasks (#6170 )	2024-11-22 17:12:30 +00:00
Linter	feat: structure auto-completion & partial `InfoTree`s	2024-11-19 09:26:58 +01:00
Meta	feat: have "motive is not type correct" come with an explanation (#6168 )	2024-11-22 23:56:17 +00:00
Parser	feat: use new `structInstFields` parser to tag structure instance fields	2024-11-19 09:26:58 +01:00
ParserCompiler
PrettyPrinter	feat: `Nat.(fold\|foldRev\|any\|all)M?` take a function which sees the upper bound (#6139 )	2024-11-22 03:05:51 +00:00
Server	refactor: make use of recursive structures in snapshot types (#6141 )	2024-11-20 15:15:14 +00:00
Util	feat: creation and reporting for asynchronous elaboration tasks (#6170 )	2024-11-22 17:12:30 +00:00
Widget	chore: rename Array.back to back! (#5897 )	2024-10-31 09:18:18 +00:00
AddDecl.lean
Attributes.lean	refactor: dead code AttributeExtensionOLeanEntry.decl (#5496 )	2024-10-01 13:34:12 +00:00
AuxRecursor.lean
BuiltinDocAttr.lean
Class.lean	chore: move `MessageData.ofConstName` earlier (#5877 )	2024-10-29 21:23:51 +00:00
Compiler.lean
CoreM.lean	feat: creation and reporting for asynchronous elaboration tasks (#6170 )	2024-11-22 17:12:30 +00:00
Data.lean	feat: add date and time functionality (#4904 )	2024-11-14 14:04:19 +00:00
Declaration.lean	feat: use "eureka!" icon for theorem completions (#5801 )	2024-10-22 10:07:37 +00:00
DeclarationRange.lean	fix: call hierarchy into `(builtin_)initialize` (#5560 )	2024-10-03 12:03:44 +00:00
DocString.lean
Elab.lean	feat: add builtin attribute to support elaboration of mutual inductives/structures (#6166 )	2024-11-22 01:48:37 +00:00
Environment.lean	chore: avoid runtime array bounds checks (#6134 )	2024-11-21 05:04:52 +00:00
Exception.lean	chore: move `MessageData.ofConstName` earlier (#5877 )	2024-10-29 21:23:51 +00:00
Expr.lean	feat: on "type mismatch" errors, expose differences in functions and pi types (#5922 )	2024-11-01 18:42:14 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean	feat: change `Array.get` to take a `Nat` and a proof (#6032 )	2024-11-12 03:30:46 +00:00
KeyedDeclsAttribute.lean
LabelAttribute.lean	chore: update copyrights (#5449 )	2024-09-24 05:27:53 +00:00
Level.lean	fix: add a missing case to `Level.geq` (#2689 )	2024-11-19 21:27:00 +00:00
Linter.lean	feat: `omit` (#5000 )	2024-08-21 13:22:34 +00:00
LoadDynlib.lean
LocalContext.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
Log.lean
Message.lean	fix: trace.profiler pretty-printing (#6138 )	2024-11-20 10:21:02 +00:00
Meta.lean
MetavarContext.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
Modifiers.lean
MonadEnv.lean	fix: bring elaborator in line with kernel for primitive projections (#5822 )	2024-10-31 03:16:52 +00:00
Parser.lean
ParserCompiler.lean
PrettyPrinter.lean	chore: move `MessageData.ofConstName` earlier (#5877 )	2024-10-29 21:23:51 +00:00
ProjFns.lean	fix: modify projection instance binder info (#5376 )	2024-09-20 06:03:59 +00:00
ReducibilityAttrs.lean
Replay.lean	chore: update copyrights (#5449 )	2024-09-24 05:27:53 +00:00
ReservedNameAction.lean
ResolveName.lean	chore: move `MessageData.ofConstName` earlier (#5877 )	2024-10-29 21:23:51 +00:00
Runtime.lean	feat: link LibUV (#4963 )	2024-08-12 12:33:24 +00:00
ScopedEnvExtension.lean
Server.lean
Structure.lean	feat: Array.insertIdx/eraseIdx take a tactic-provided proof (#6133 )	2024-11-20 09:52:38 +00:00
SubExpr.lean	chore: cleanup imports (#5825 )	2024-10-23 23:51:13 +00:00
Syntax.lean	chore: avoid runtime array bounds checks (#6134 )	2024-11-21 05:04:52 +00:00
ToExpr.lean	refactor: redefine unsigned fixed width integers in terms of BitVec (#5323 )	2024-10-16 07:28:23 +00:00
Util.lean	feat: localize universe metavariable errors at `let` bindings and `fun` binders (#5402 )	2024-09-24 05:30:42 +00:00
Widget.lean