diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index e4f9f8cd76..a368f8a79a 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -296,7 +296,7 @@ macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y) macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y) macro_rules | `($x / $y) => `(binop% HDiv.hDiv $x $y) macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y) --- exponentiation should be considered a right action (#2220) +-- exponentiation should be considered a right action (#2854) macro_rules | `($x ^ $y) => `(rightact% HPow.hPow $x $y) macro_rules | `($x ++ $y) => `(binop% HAppend.hAppend $x $y) macro_rules | `(- $x) => `(unop% Neg.neg $x) diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 3346e79e5f..fd03c0f9f0 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types: - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand). Only `a` participates in the protocol since `b` can have an unrelated type. This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real` - exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220) + exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854) - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`). The elaborator works as follows: @@ -449,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`. It is similar to how `binop% R x y` elaborates but with a significant difference: - it does not use the expected type when computing the types of the operads. + it does not use the expected type when computing the types of the operands. - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y` is `Prop` they are coerced to `Bool`. This is used for relations such as `==` which do not support `Prop`, but we still want diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 8ac6f2b9c6..21fb2df03f 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -517,15 +517,15 @@ def appendOptMessageData (m : MessageData) (header : String) (m? : Option Messag def reportDiag : MetaM Unit := do if (← isDiagnosticsEnabled) then - let threshould := diag.threshold.get (← getOptions) - let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshould - let heu? := mkMessageBodyFor? (← get).diag.heuristicCounter threshould - let inst? := mkMessageBodyFor? (← get).diag.instanceCounter threshould + let threshold := diag.threshold.get (← getOptions) + let unfold? := mkMessageBodyFor? (← get).diag.unfoldCounter threshold + let heu? := mkMessageBodyFor? (← get).diag.heuristicCounter threshold + let inst? := mkMessageBodyFor? (← get).diag.instanceCounter threshold if unfold?.isSome || heu?.isSome || inst?.isSome then let m := appendOptMessageData MessageData.nil "unfolded declarations:" unfold? let m := appendOptMessageData m "used instances:" inst? let m := appendOptMessageData m "`isDefEq` heuristic:" heu? - let m := m ++ "\nuse `set_option diag.threshould ` to control threshold for reporting counters" + let m := m ++ "\nuse `set_option diag.threshold ` to control threshold for reporting counters" logInfo m def getLocalInstances : MetaM LocalInstances := diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index ae561c31a9..ea219c659d 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -2013,7 +2013,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD we only want to unify negation (and not all other field operations as well). Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986 - Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure. + Note that we use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure. We added this refinement to address a performance issue in code such as ``` let val : Test := bar c1 key diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index e920989533..ee84d98b49 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -344,7 +344,7 @@ inductive ProjReductionKind where | yesWithDelta /-- Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process. - Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`. + Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`. This option is stronger than `yes`, but weaker than `yesWithDelta`. We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations. When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`, diff --git a/tests/lean/hpow.lean b/tests/lean/hpow.lean index 86980af748..6dd24d41c3 100644 --- a/tests/lean/hpow.lean +++ b/tests/lean/hpow.lean @@ -1,7 +1,7 @@ import Lean.Data.Rat /-! -Test the `rightact%` elaborator for `HPow.hPow`, added to address #2220 +Test the `rightact%` elaborator for `HPow.hPow`, added to address #2854 -/ open Lean diff --git a/tests/lean/run/diagRec.lean b/tests/lean/run/diagRec.lean index a3ee0823b9..5592499024 100644 --- a/tests/lean/run/diagRec.lean +++ b/tests/lean/run/diagRec.lean @@ -14,7 +14,7 @@ info: unfolded declarations: Or.rec ↦ 144 PProd.fst ↦ 126 Acc.rec ↦ 108 -use `set_option diag.threshould ` to control threshold for reporting counters +use `set_option diag.threshold ` to control threshold for reporting counters -/ #guard_msgs in set_option diag true in