max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Kim Morrison da32bdd79c
chore: additional newline before 'additional diagnostic information' message (#7169) 
This PR adds an addition newline before the "Additional diagnostic
information may be available using the `set_option ... true` command."
messages, to provide better visual separation from the main error
message.
2025-02-23 23:27:33 +00:00
..
Compiler feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Data fix: do not cancel async elaboration tasks (#7175) 2025-02-21 17:24:36 +00:00
DocString fix: Lake: brittle dependency on env ext name 2024-10-07 13:26:07 +02:00
Elab chore: post-#7100 cleanup (#7196) 2025-02-23 22:46:22 +00:00
Language fix: do not cancel async elaboration tasks (#7175) 2025-02-21 17:24:36 +00:00
Linter perf: optimize sorry detection in unused variables linter (#7129) 2025-02-22 16:43:39 +00:00
Meta feat: simp diagnostics in grind (#6902) 2025-02-23 17:55:17 +00:00
Parser feat: make structure parent projections nameable (#7100) 2025-02-18 07:38:13 +00:00
ParserCompiler
PrettyPrinter feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Server perf: optimize sorry detection in unused variables linter (#7129) 2025-02-22 16:43:39 +00:00
Util feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Widget feat: more robust server parallelism (#7087) 2025-02-20 10:54:22 +00:00
AddDecl.lean chore: don't forget about namespace reservation for async-unsupported constant kinds (#6987) 2025-02-22 16:45:40 +00:00
Attributes.lean refactor: dead code AttributeExtensionOLeanEntry.decl (#5496) 2024-10-01 13:34:12 +00:00
AuxRecursor.lean refactor: IndGroupInst.brecOn (#4787) 2024-07-19 10:20:50 +00:00
BuiltinDocAttr.lean
Class.lean chore: move MessageData.ofConstName earlier (#5877) 2024-10-29 21:23:51 +00:00
Compiler.lean
CoreM.lean chore: additional newline before 'additional diagnostic information' message (#7169) 2025-02-23 23:27:33 +00:00
Data.lean feat: add date and time functionality (#4904) 2024-11-14 14:04:19 +00:00
Declaration.lean feat: add support for constructors and axioms to the grind E-matching module (#6839) 2025-01-29 05:22:05 +00:00
DeclarationRange.lean feat: labeled and unique sorries (#5757) 2024-12-11 23:53:02 +00:00
DocString.lean feat: recommended_spelling command (#6869) 2025-02-03 11:15:52 +00:00
Elab.lean feat: #info_trees in command (#6964) 2025-02-06 03:11:53 +00:00
Environment.lean feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Exception.lean fix: convert kernel interrupt into elab interrupt (#6988) 2025-02-07 15:55:32 +00:00
Expr.lean fix: FunInd to clear match discriminants if possible 2025-02-17 18:21:10 +01: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 feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +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 feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
Log.lean
Message.lean feat: generalize infoview.maxTraceChildren to the cmdline (#6716) 2025-01-21 02:06:24 +00:00
Meta.lean feat: binderNameHint (#6947) 2025-02-06 11:03:27 +00:00
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 feat: Environment.addConstAsync (#6691) 2025-01-19 02:00:16 +00:00
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 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 feat: do not propagate pretty printer errors through messages (#3696) 2024-12-11 04:10:09 +00:00
PrivateName.lean feat: Environment.addConstAsync (#6691) 2025-01-19 02:00:16 +00:00
ProjFns.lean fix: modify projection instance binder info (#5376) 2024-09-20 06:03:59 +00:00
ReducibilityAttrs.lean
Replay.lean chore: trivial changes from async-proofs branch (#7028) 2025-02-10 16:44:05 +00:00
ReservedNameAction.lean
ResolveName.lean fix: when pretty printing constant names, do not use aliases from "non-API exports" (#5689) 2024-12-10 17:50:50 +00:00
Runtime.lean feat: link LibUV (#4963) 2024-08-12 12:33:24 +00:00
ScopedEnvExtension.lean
Server.lean fix: do not cancel async elaboration tasks (#7175) 2025-02-21 17:24:36 +00:00
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 feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
ToExpr.lean feat: upstream ToExpr deriving handler from Mathlib (#6473) 2024-12-31 15:11:53 +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