max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive/Diff.lean.expected.out
Ed Ayers 2a6697e077
feat: goal-diffs (#1610)
2022-09-24 11:46:11 +02:00

267 lines
17 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.

{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Nat"),
names := #["x"],
isInserted? := some true,
isRemoved? := none }] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", highlightColor? := some "red" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Nat"),
names := #["x"],
isInserted? := none,
isRemoved? := none }] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.text "∀ (",
Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " : ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0", highlightColor? := some "red" }
(Lean.Widget.TaggedText.text "Nat"),
Lean.Widget.TaggedText.text "), ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0", highlightColor? := some "red" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "True")])]),
isInserted? := some false,
isRemoved? := none,
hyps := #[] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Sort u_1"),
names := #["α"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Nat"),
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", highlightColor? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", highlightColor? := some "yellow" }
(Lean.Widget.TaggedText.text "y")])]),
names := #["f"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "y"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
names := #["h"],
isInserted? := none,
isRemoved? := none }] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Sort u_1"),
names := #["α"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Nat"),
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", highlightColor? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", highlightColor? := some "green" }
(Lean.Widget.TaggedText.text "x")])]),
names := #["f"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "y"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
names := #["h"],
isInserted? := none,
isRemoved? := none }] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := some "yellow" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
Lean.Widget.TaggedText.text " ∧ ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
isInserted? := none,
isRemoved? := some true,
hyps := #[] },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
isInserted? := none,
isRemoved? := none,
hyps := #[] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "True"),
isInserted? := none,
isRemoved? := some true,
hyps := #[] }] }
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1/0/1", highlightColor? := some "yellow" }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " + ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1/1", highlightColor? := some "yellow" }
(Lean.Widget.TaggedText.text "z")]),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "z"),
Lean.Widget.TaggedText.text " + ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "y")])]),
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.text "Nat"),
names := #["x", "y", "z"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", highlightColor? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "y"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", highlightColor? := none }
(Lean.Widget.TaggedText.text "x")]),
names := #["h"],
isInserted? := none,
isRemoved? := none }] }] }
Reference in a new issue View git blame Copy permalink