max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use emoji variant of ✅️,❌️,💥️ (#5173)

Browse source 
First part of #5015, using emoji variant of unicode symbols for
✅️,❌️,💥️.

---

(Partially) closes #5015
This commit is contained in:
Jon Eugster 2024-08-26 21:46:37 +02:00 • committed by GitHub
parent f917f811c8
commit c45a6a93f9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 95 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/GuardMsgs.lean
View file

@ -163,7 +163,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
let diff := Diff.diff (expected.split (· == '\n')).toArray (res.split (· == '\n')).toArray
Diff.linesToString diff
else res
logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"
logErrorAt tk m!"❌️ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"
pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
| _ => throwUnsupportedSyntax

8
src/Lean/Util/Trace.lean
View file

@ -294,9 +294,9 @@ macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
if (← Lean.isTracingEnabledFor cls) then
Lean.addTrace cls $msg)
def bombEmoji := "💥"
def checkEmoji := "✅"
def crossEmoji := "❌"
def bombEmoji := "💥️"
def checkEmoji := "✅️"
def crossEmoji := "❌️"
def exceptBoolEmoji : Except ε Bool → String
| .error _ => bombEmoji
@ -326,7 +326,7 @@ instance : ExceptToEmoji ε (Option α) where
Similar to `withTraceNode`, but msg is constructed **before** executing `k`.
This is important when debugging methods such as `isDefEq`, and we want to generate the message
before `k` updates the metavariable assignment. The class `ExceptToEmoji` is used to convert
the result produced by `k` into an emoji (e.g., `💥`, `✅`, `❌`).
the result produced by `k` into an emoji (e.g., `💥️`, `✅️`, `❌️`).
TODO: find better name for this function.
-/

8
tests/lean/366.lean.expected.out
View file

@ -1,7 +1,7 @@
[Meta.synthInstance] ✅ Inhabited Nat
[Meta.synthInstance] ✅️ Inhabited Nat
[Meta.synthInstance] new goal Inhabited Nat
[Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
[Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
[Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
[Meta.synthInstance.answer] ✅ Inhabited Nat
[Meta.synthInstance] ✅️ apply instInhabitedNat to Inhabited Nat
[Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat
[Meta.synthInstance.answer] ✅️ Inhabited Nat
[Meta.synthInstance] result instInhabitedNat

137
tests/lean/815b.lean.expected.out
View file

@ -5,19 +5,19 @@
815b.lean:9:9-9:13: warning: declaration uses 'sorry'
815b.lean:10:9-10:13: warning: declaration uses 'sorry'
815b.lean:11:9-11:13: warning: declaration uses 'sorry'
[Meta.synthInstance] ✅ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] ✅️ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
[Meta.synthInstance] ✅ apply @swap to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth f
[Meta.synthInstance] ✅ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance.unusedArgs] α → IsSmooth f
has unused arguments, reduced type
IsSmooth f
@ -25,9 +25,9 @@
fun redf a => redf
[Meta.synthInstance] new goal IsSmooth f
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance] ✅ apply inst✝ to IsSmooth f
[Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f
[Meta.synthInstance.answer] ✅ IsSmooth f
[Meta.synthInstance] ✅️ apply inst✝ to IsSmooth f
[Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
[Meta.synthInstance.answer] ✅️ IsSmooth f
[Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] α → IsSmooth f
@ -45,24 +45,24 @@
fun redf a => redf
[Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance] ❌ apply inst✝ to ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.tryResolve] ❌ IsSmooth (f b) ≟ IsSmooth f
[Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) ≟ IsSmooth f
[Meta.synthInstance] ✅ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
[Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
[Meta.synthInstance] ✅ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance.unusedArgs] α → δ → IsSmooth f
has unused arguments, reduced type
IsSmooth f
@ -76,24 +76,25 @@
∀ (b : β), IsSmooth (f b)
Transformer
fun redf a a => redf
[Meta.synthInstance] ❌ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
[Meta.synthInstance] ✅ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a)
has unused arguments, reduced type
∀ (a : α), IsSmooth fun g => f (g a)
Transformer
fun redf a a_1 => redf a
[Meta.synthInstance] ❌ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
[Meta.synthInstance] ❌ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
[Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g =>
[Meta.synthInstance] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
[Meta.synthInstance] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
[Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
[Meta.synthInstance] ✅ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
[Meta.synthInstance] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
[Meta.synthInstance.unusedArgs] α → IsSmooth f
has unused arguments, reduced type
IsSmooth f
@ -104,15 +105,15 @@
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth f
[Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g =>
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
[Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
[Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
[Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
has unused arguments, reduced type
IsSmooth fun g => g
@ -120,21 +121,21 @@
fun redf a => redf
[Meta.synthInstance] new goal IsSmooth fun g => g
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth f
[Meta.synthInstance] ✅ apply @swap to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
[Meta.synthInstance] ❌ apply @diag to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
[Meta.synthInstance] ❌ apply @comp to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
[Meta.synthInstance] ❌ apply @parm to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
[Meta.synthInstance] ❌ apply @const to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
[Meta.synthInstance] ✅ apply @identity to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a
[Meta.synthInstance.answer] ✅ IsSmooth fun g => g
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
[Meta.synthInstance] ❌️ apply @diag to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
[Meta.synthInstance] ❌️ apply @comp to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
[Meta.synthInstance] ❌️ apply @parm to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
[Meta.synthInstance] ❌️ apply @const to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
[Meta.synthInstance] ✅️ apply @identity to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun a => a
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun a =>
a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 1
@ -146,11 +147,11 @@
[Meta.synthInstance.resume] propagating α →
IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
[Meta.synthInstance.resume] size: 3
[Meta.synthInstance.answer] ✅ IsSmooth fun g => g
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun b a =>
b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 4
@ -162,23 +163,23 @@
[Meta.synthInstance.resume] propagating α →
IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 8
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating α →
IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
[Meta.synthInstance.resume] size: 6
[Meta.synthInstance.answer] ✅ IsSmooth fun g a => f (g a) d
[Meta.synthInstance.answer] ✅️ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] result swap fun a g => f (g a) d

4
tests/lean/973b.lean.expected.out
View file

@ -1,5 +1,5 @@
973b.lean:5:8-5:10: warning: declaration uses 'sorry'
973b.lean:9:8-9:11: warning: declaration uses 'sorry'
[Meta.Tactic.simp.discharge] ex discharge ❌
[Meta.Tactic.simp.discharge] ex discharge ❌️
?p x
[Meta.Tactic.simp.discharge] ex discharge ❌ ?p (f x)
[Meta.Tactic.simp.discharge] ex discharge ❌️ ?p (f x)

4
tests/lean/etaReducedMvarAssignments.lean.expected.out
View file

@ -1,4 +1,4 @@
Pi.hasLe : LE ((i : ι) → α i)
[Meta.isDefEq.assign] ✅ ?m i := α i
[Meta.isDefEq.assign] ✅️ ?m i := α i
[Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
[Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)
[Meta.isDefEq.assign.checkTypes] ✅️ (?m : ι → Type ?u) := (α : ι → Type v)

4
tests/lean/infoFromFailure.lean.expected.out
View file

@ -1,9 +1,9 @@
B.foo "hello" : String × String
[Meta.synthInstance] ❌ Add String
[Meta.synthInstance] ❌️ Add String
[Meta.synthInstance] no instances for Add String
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌ Add Bool
[Meta.synthInstance] ❌️ Add Bool
[Meta.synthInstance] no instances for Add Bool
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] result <not-available>

6
tests/lean/run/1234.lean
View file

@ -10,7 +10,7 @@ set_option trace.Meta.Tactic.simp true
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
@ -35,7 +35,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
@ -58,7 +58,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v

2
tests/lean/run/1380.lean
View file

@ -12,7 +12,7 @@ info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
?a = ?a
with
v₂ = v₁
[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅
[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅️
v₁ < v₂
[Meta.Tactic.simp.rewrite] hv:1000, v₁ < v₂ ==> True
[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000, v₂ = v₁ ==> False

2
tests/lean/run/3257.lean
View file

@ -14,7 +14,7 @@ example : U := by
simp [foo, T.mk]
/--
info: [Meta.Tactic.simp.discharge] bar discharge ✅
info: [Meta.Tactic.simp.discharge] bar discharge ✅️
autoParam T _auto✝
[Meta.Tactic.simp.rewrite] T.mk:1000, T ==> True
[Meta.Tactic.simp.rewrite] bar:1000, U ==> True

12
tests/lean/run/guard_msgs.lean
View file

@ -8,7 +8,7 @@ example : α := x
/--
error: unknown identifier 'x'
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
error: unknown identifier 'x'
-/
@ -62,7 +62,7 @@ example : α := 22
info: foo ⏎
bar
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
info: foo ⏎
bar
@ -83,7 +83,7 @@ run_meta Lean.logInfo "foo \nbar"
info: foo ⏎⏎
bar
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
info: foo ⏎⏎
bar
@ -170,7 +170,7 @@ info: ABCDEFG
HIJKLMNOP
QRSTUVWXYZ
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
-
+ info: ABCDEFG
@ -187,7 +187,7 @@ info: ABCDEFG
HIJKLMNOP
QRSTUVWXYZ
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
info: ABCDEFG
+ HIJKLMNOP
@ -237,7 +237,7 @@ info: Tree.branch
4
(Tree.branch (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)) 2 (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
---
error: ❌ Docstring on `#guard_msgs` does not match generated message:
error: ❌️ Docstring on `#guard_msgs` does not match generated message:
info: Tree.branch
(Tree.branch