max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive/plainGoal.lean.expected.out
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

179 lines
9.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 0, "character": 20}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
"goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 0, "character": 21}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
"goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 3, "character": 2}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
"goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 3, "character": 3}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 7, "character": 3}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 10, "character": 20}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
"goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 15, "character": 9}}
{"rendered": "```lean\ncase zero\n⊢ 0 + 0 = 0\n```",
"goals": ["case zero\n⊢ 0 + 0 = 0"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 17, "character": 5}}
{"rendered":
"```lean\ncase succ\nn✝ : Nat\na✝ : 0 + n✝ = n✝\n⊢ 0 + (n✝ + 1) = n✝ + 1\n```",
"goals": ["case succ\nn✝ : Nat\na✝ : 0 + n✝ = n✝\n⊢ 0 + (n✝ + 1) = n✝ + 1"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 21, "character": 9}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 21, "character": 10}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 21, "character": 11}}
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 27, "character": 3}}
{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
"goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 27, "character": 9}}
{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m\n```",
"goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 27, "character": 13}}
{"rendered": "no goals", "goals": []}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 34, "character": 3}}
{"rendered": "```lean\ncase zero\n⊢ 0 + 0 = 0\n```",
"goals": ["case zero\n⊢ 0 + 0 = 0"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 40, "character": 3}}
{"rendered":
"```lean\ncase zero\n⊢ 0 + 0 = 0\n```\n---\n```lean\ncase succ\nn✝ : Nat\na✝ : 0 + n✝ = n✝\n⊢ 0 + (n✝ + 1) = n✝ + 1\n```",
"goals":
["case zero\n⊢ 0 + 0 = 0",
"case succ\nn✝ : Nat\na✝ : 0 + n✝ = n✝\n⊢ 0 + (n✝ + 1) = n✝ + 1"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 44, "character": 3}}
{"rendered":
"```lean\ncase zero\n⊢ 0 + 0 = 0\n```\n---\n```lean\ncase succ\nn✝ : Nat\n⊢ 0 + (n✝ + 1) = n✝ + 1\n```",
"goals":
["case zero\n⊢ 0 + 0 = 0", "case succ\nn✝ : Nat\n⊢ 0 + (n✝ + 1) = n✝ + 1"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 48, "character": 3}}
{"rendered": "```lean\na b : Nat\n⊢ a = b\n```",
"goals": ["a b : Nat\n⊢ a = b"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 51, "character": 20}}
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
"goals": ["α : Sort ?u\n⊢ α → α"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 55, "character": 3}}
{"rendered":
"```lean\nα : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a\n```",
"goals":
["α : Sort u_1\np : α → Prop\na b : α\ninst✝ : DecidablePred p\nh : ∀ {p : α → Prop} [inst : DecidablePred p], p a → p b\n⊢ p a"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 61, "character": 3}}
{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 63, "character": 3}}
{"rendered": "```lean\ncase right\n⊢ False\n```",
"goals": ["case right\n⊢ False"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 68, "character": 3}}
{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 70, "character": 3}}
{"rendered": "```lean\ncase right\n⊢ False\n```",
"goals": ["case right\n⊢ False"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 78, "character": 29}}
{"rendered":
"```lean\nt a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * (n✝ + 1)\n```\n---\n```lean\nt a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```\n---\n```lean\nt a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)\n```",
"goals":
["t a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + t * (n✝ + 1)",
"t a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)",
"t a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 82, "character": 53}}
{"rendered":
"```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
"goals":
["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 82, "character": 54}}
{"rendered":
"```lean\ncase nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```",
"goals":
["case nil\nα : Type u_1\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 86, "character": 38}}
{"rendered": "no goals", "goals": []}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 89, "character": 39}}
null
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 93, "character": 16}}
{"rendered":
"```lean\ncase left\n⊢ True\n```\n---\n```lean\ncase right\n⊢ False\n```",
"goals": ["case left\n⊢ True", "case right\n⊢ False"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 97, "character": 8}}
{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 99, "character": 4}}
{"rendered": "```lean\n| True = True\n```", "goals": ["| True = True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 101, "character": 2}}
{"rendered": "no goals", "goals": []}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 106, "character": 4}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 108, "character": 2}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 113, "character": 4}}
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 115, "character": 2}}
null
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 120, "character": 2}}
{"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 124, "character": 17}}
{"rendered": "```lean\np q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q\n```",
"goals": ["p q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 128, "character": 18}}
{"rendered": "```lean\np q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)\n```",
"goals": ["p q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 133, "character": 3}}
{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 133, "character": 4}}
{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 139, "character": 34}}
{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 142, "character": 34}}
{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
{"textDocument": {"uri": "file:///plainGoal.lean"},
"position": {"line": 145, "character": 34}}
{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
Reference in a new issue View git blame Copy permalink