max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Leonardo de Moura e3578c2f36
fix: discrepancy theorem vs example (#4493) 
When the type of an `example` is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.

Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for examples when
their type was a proposition.
This discrepancy often confused users.

Additionally, we considered extending the above behavior to definitions
when
1- When their type is a proposition. However, it still caused disruption
in Mathlib.
2- When their type is provided. That is, we would keep the current
behavior only if `: <type>` was omitted. This would make the elaborator
for `def` much closer to the one for `theorem`, but it proved to be too
restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
  ⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
  ⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.

closes #4398
closes #4482 Remark: PR #4482 implements option 1 above. We may consider
it again in the future.
2024-06-24 01:18:41 +00:00
..
Compiler feat: expose flags for the bundled C compiler (#4477) 2024-06-22 01:23:33 +00:00
Data chore: cleanup PersistentHashMap.lean 2024-06-19 20:21:34 +02:00
DocString feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Elab fix: discrepancy theorem vs example (#4493) 2024-06-24 01:18:41 +00:00
Language chore: slightly more informative trace.Elab.snapshotTree 2024-06-11 10:44:04 +02:00
Linter feat: add a linter for local vars that clash with their constructors (#4301) 2024-06-14 13:03:09 +00:00
Meta fix: cached results at synthInstance? (#4530) 2024-06-23 17:54:35 +00:00
Parser feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
ParserCompiler feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
PrettyPrinter chore: missing registerTraceClass (#4369) 2024-06-06 00:53:16 +00:00
Server feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Util chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
Widget feat: widget messages (#4254) 2024-05-29 06:37:42 +00:00
AddDecl.lean feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
Attributes.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
AuxRecursor.lean refactor: constructions: modify environment in lean world (#4474) 2024-06-19 08:58:53 +00:00
BuiltinDocAttr.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Class.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Compiler.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CoreM.lean fix: incorrect info tree reuse (#4340) 2024-06-04 09:28:40 +00:00
Data.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Declaration.lean refactor: constructions: modify environment in lean world (#4474) 2024-06-19 08:58:53 +00:00
DeclarationRange.lean feat: snapshot trees and language processors (#3014) 2024-03-14 13:40:08 +00:00
DocString.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Elab.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
Environment.lean doc: more detailed docstring for PersistentEnvExtension (#4501) 2024-06-21 08:34:04 +00:00
Eval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Exception.lean feat: apply’s error message should show implicit arguments as needed (#3929) 2024-05-18 06:25:43 +00:00
Expr.lean feat: shorten auto-generated instance names (#3089) 2024-04-13 18:08:50 +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 perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
KeyedDeclsAttribute.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LabelAttribute.lean chore: reorganising to reduce imports (#3790) 2024-03-27 11:15:01 +00:00
LazyInitExtension.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Level.lean chore: remove partial TODO (#4380) 2024-06-06 18:04:55 +00:00
Linter.lean feat: add a linter for local vars that clash with their constructors (#4301) 2024-06-14 13:03:09 +00:00
LoadDynlib.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LocalContext.lean chore: upstream omega (#3367) 2024-02-19 00:19:55 +00:00
Log.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Message.lean feat: default pp if pp expr/syntax/level without context (#4433) 2024-06-14 08:55:49 +00:00
Meta.lean feat: improve set_option diagnostics true (#4031) 2024-04-30 05:07:03 +00:00
MetavarContext.lean fix: eta reduce mvar assignments in isDefEq (#4387) 2024-06-18 23:41:40 +00:00
Modifiers.lean refactor: constructions: modify environment in lean world (#4474) 2024-06-19 08:58:53 +00:00
MonadEnv.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Parser.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
ParserCompiler.lean refactor: Offset.lean and related files (#3614) 2024-03-05 19:40:15 -08:00
PrettyPrinter.lean feat: use lazy MessageData for omega errors (#4360) 2024-06-14 20:21:37 +00:00
ProjFns.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ReducibilityAttrs.lean chore: fix linter errors (#4502) 2024-06-19 18:24:08 +00:00
Replay.lean feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
ReservedNameAction.lean fix: FunInd: support structural recursion on reflexive types (#4327) 2024-06-05 07:54:48 +00:00
ResolveName.lean feat: open _root_.<namespace> (#4505) 2024-06-19 21:59:46 +00:00
Runtime.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ScopedEnvExtension.lean feat: flexible reducibility attributes 2024-04-29 05:46:11 +02:00
Server.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Structure.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SubExpr.lean fix: use correct expr positions when delaborating match patterns (#4034) 2024-05-01 12:02:10 +00:00
Syntax.lean fix: incremental reuse leading to goals in front of the text cursor being shown (#4395) 2024-06-08 15:08:14 +00:00
ToExpr.lean feat: support idents in auto tactics (#3328) 2024-05-03 04:37:07 +00:00
Util.lean chore: upstream exact? and apply? from Std (#3447) 2024-02-23 21:55:24 +00:00
Widget.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00