mystery guest

Stream: mathlib4

[Johan Commelin]

I have a file with

import Mathlib

#check instENatCanonicallyOrderedCommSemiring
-- instENatCanonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℕ∞

but I can not jump to definition on instENatCanonicallyOrderedCommSemiring and I can also not find that declaration by grepping for it... what's going on?

[Markus Himmel]

It's from https://github.com/leanprover-community/mathlib4/blob/2959869cae3984b89b9038d57e2b3865a23c59a1/Mathlib/Data/ENat/Basic.lean#L27

[Johan Commelin]

Aah! Thanks

[Johan Commelin]

1. How did you find it?
2. Should jump to definition jump to that line?

[Johan Commelin]

3. Should it be listed in the docs?

[Markus Himmel]

1. I put instENatCanonicallyOrderedCommSemiring into Loogle, which sent me to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/ENat/Basic.html#instENatCanonicallyOrderedCommSemiring which doesn't show it on the page (I have had this before with deriving ... for ...), so I looked at the source of the file.
2. I think it would be good to report this to lean4
3. I think it would be good to report this to doc-gen

[Kyle Miller]

This should be fixed in lean4#5899

[Kyle Miller]

There are still a number of instances from deriving handlers that are missing declaration range information, so be sure to report further issues like this!

[Damiano Testa]

I am not sure if these count as missing declaration ranges, but notation does not produce a selectionRange, while, for instance, syntax does.

import Lean.Elab.Command

notation "NN" => Nat

syntax "NNstx" : term

open Lean

/--
info: termNN
(⟨1, 0⟩, ⟨1, 0⟩)
(⟨3, 0⟩, ⟨3, 20⟩)
---
info: termNNstx
(⟨5, 0⟩, ⟨5, 6⟩)
(⟨5, 0⟩, ⟨5, 21⟩)
-/
#guard_msgs in
run_cmd
  let nms := [`termNN, `termNNstx]
  for nm in nms do
    let rgs := (← findDeclarationRanges? nm).getD default
    logInfo m!"{nm}\n\
              {(rgs.selectionRange.pos, rgs.selectionRange.endPos)}\n\
              {(rgs.range.pos, rgs.range.endPos)}"

I would have guessed that notation would also assign notation as the selectionRange for NN, analogously to what syntax does.

[Johan Commelin]

cc @Kyle Miller, I guess....