max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Sebastian Graf e886373dc8
fix: Avoid a type error in mvcgen and turn fewer natural goals into synthetic opaque ones (#9045) 
This PR fixes a type error in `mvcgen` and makes it turn fewer natural
goals into synthetic opaque ones, so that tactics such as `trivial` may
instantiate them more easily.

---------

Co-authored-by: Sebastian Graf <sg@lean-fro.org>
2025-06-27 16:27:06 +00:00
..
Compiler perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
Data feat: linter.loopingSimpArgs (#8865) 2025-06-23 07:36:21 +00:00
DocString perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
Elab fix: Avoid a type error in mvcgen and turn fewer natural goals into synthetic opaque ones (#9045) 2025-06-27 16:27:06 +00:00
ErrorExplanations feat: improve projection and field-notation errors (#8986) 2025-06-26 18:36:47 +00:00
Language feat: server support for new module setup (#8699) 2025-06-23 18:00:14 +00:00
Linter chore: use note and hint' for message addenda (#8980) 2025-06-27 15:16:01 +00:00
Meta feat: Toint inequalities in cutsat (#9026) 2025-06-27 06:29:31 +00:00
Parser chore: reserve public section syntax (#9032) 2025-06-27 12:21:01 +00:00
ParserCompiler
PrettyPrinter fix: apply newlines before and after comments when formatting syntax (#8626) 2025-06-26 19:23:35 +00:00
Server fix: highlight keywords when keyword is actual identifier (#9019) 2025-06-27 08:23:10 +00:00
Util feat: server support for new module setup (#8699) 2025-06-23 18:00:14 +00:00
Widget feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804) 2025-06-22 21:54:57 +00:00
AddDecl.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
Attributes.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
AuxRecursor.lean refactor: remove binductionOn, use brecOn instead (#8820) 2025-06-17 07:07:24 +00:00
BuiltinDocAttr.lean chore: follow up on #8173 post-stage0 update (#8722) 2025-06-16 09:08:35 +00:00
Class.lean doc: add documentation for builtin attributes (#8173) 2025-06-11 09:04:37 +00:00
Compiler.lean feat: meta phase restrictions 2025-06-12 16:36:08 +02:00
CoreM.lean chore: use note and hint' for message addenda (#8980) 2025-06-27 15:16:01 +00:00
Data.lean chore: remove the old Lean.Data.HashMap implementation (#7519) 2025-03-20 23:49:55 +00:00
Declaration.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
DeclarationRange.lean refactor: environment extension state splitting (#8653) 2025-06-11 12:52:04 +00:00
DefEqAttrib.lean feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
DocString.lean feat: language reference links and examples in docstrings (#7240) 2025-03-12 09:17:27 +00:00
Elab.lean feat: add elaborators, completions, and hovers for named errors (#8730) 2025-06-18 15:51:34 +00:00
EnvExtension.lean refactor: environment extension state splitting (#8653) 2025-06-11 12:52:04 +00:00
Environment.lean perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
ErrorExplanation.lean feat: add elaborators, completions, and hovers for named errors (#8730) 2025-06-18 15:51:34 +00:00
ErrorExplanations.lean feat: improve projection and field-notation errors (#8986) 2025-06-26 18:36:47 +00:00
Exception.lean feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
Expr.lean feat: (commutative) semiring support in grind (#8921) 2025-06-21 23:00:16 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean fix: block adversarial exploit of non-aborting assert! (#8559) 2025-05-31 00:08:30 +00:00
Linter.lean feat: linter.unusedSimpArgs (#8901) 2025-06-22 09:10:21 +00:00
LoadDynlib.lean feat: smarter plugin loading (#7090) 2025-02-18 23:03:52 +00:00
LocalContext.lean feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804) 2025-06-22 21:54:57 +00:00
Log.lean feat: add initial error explanations (#8934) 2025-06-23 17:24:09 +00:00
Message.lean feat: improve projection and field-notation errors (#8986) 2025-06-26 18:36:47 +00:00
Meta.lean feat: add Meta.letToHave and the let_to_have tactic (#8954) 2025-06-24 01:33:53 +00:00
MetavarContext.lean feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804) 2025-06-22 21:54:57 +00:00
Modifiers.lean feat: allow access to private names through import all (#8828) 2025-06-27 12:13:46 +00:00
MonadEnv.lean feat: meta phase restrictions 2025-06-12 16:36:08 +02:00
Namespace.lean refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794) 2025-04-02 16:19:12 +00:00
Parser.lean
ParserCompiler.lean feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804) 2025-06-22 21:54:57 +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 chore: use note and hint' for message addenda (#8980) 2025-06-27 15:16:01 +00:00
Replay.lean chore: Mathlib fixes (#7327) 2025-03-04 13:41:30 +00:00
ReservedNameAction.lean feat: make equational theorems of non-exposed defs private (#8519) 2025-06-04 11:52:08 +00:00
ResolveName.lean feat: allow access to private names through import all (#8828) 2025-06-27 12:13:46 +00:00
Runtime.lean
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
Setup.lean perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
Shell.lean feat: ignore lean -R if module name is in setup (#8874) 2025-06-23 17:55:52 +00:00
Structure.lean refactor: factor out common code for structure default values (#7737) 2025-03-31 22:40:39 +00:00
SubExpr.lean fix: replace bad simp lemmas for Id (#7352) 2025-05-22 22:45:35 +00:00
Syntax.lean fix: replace bad simp lemmas for Id (#7352) 2025-05-22 22:45:35 +00:00
ToExpr.lean feat: ToExpr IntX (#7268) 2025-02-28 09:32:30 +00:00
ToLevel.lean
Util.lean feat: server support for new module setup (#8699) 2025-06-23 18:00:14 +00:00
Widget.lean