feat: signature pretty printer for hovers
This commit is contained in:
Sebastian Ullrich
Gabriel Ebner
parent
533c770e36
commit
b6bd2dea35
11 changed files with 118 additions and 45 deletions
|
|
@ -59,6 +59,14 @@ def ppCommand (stx : Syntax.Command) : CoreM Format := ppCategory `command stx
|
|||
def ppModule (stx : TSyntax ``Parser.Module.module) : CoreM Format := do
|
||||
parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
|
||||
|
||||
open Delaborator in
|
||||
/-- Pretty-prints a declaration `c` as `c.{<levels>} <params> : <type>`. -/
|
||||
def ppSignature (c : Name) : MetaM FormatWithInfos := do
|
||||
let decl ← getConstInfo c
|
||||
let e := .const c (decl.levelParams.map mkLevelParam)
|
||||
let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
|
||||
return ⟨← ppTerm ⟨stx⟩, infos⟩ -- HACK: not a term
|
||||
|
||||
private partial def noContext : MessageData → MessageData
|
||||
| MessageData.withContext _ msg => noContext msg
|
||||
| MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
|
||||
|
|
|
|||
|
|
@ -284,7 +284,9 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
|
|||
trace[PrettyPrinter.delab.input] "{Std.format e}"
|
||||
let mut opts ← getOptions
|
||||
-- default `pp.proofs` to `true` if `e` is a proof
|
||||
if pp.proofs.get? opts == none then
|
||||
if pp.proofs.get? opts == none &&
|
||||
-- necessary for `delabConstWithSignature`, and harmless otherwise
|
||||
!e.isConst then
|
||||
try if ← Meta.isProof e then opts := pp.proofs.set opts true
|
||||
catch _ => pure ()
|
||||
withOptions (fun _ => opts) do
|
||||
|
|
|
|||
|
|
@ -763,4 +763,52 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do
|
|||
@[builtin_delab app.Lean.Name.num]
|
||||
def delabNameMkNum : Delab := delabNameMkStr
|
||||
|
||||
open Parser Command Term in
|
||||
@[run_builtin_parser_attribute_hooks]
|
||||
-- use `termParser` instead of `declId` so we can reuse `delabConst`
|
||||
def declSigWithId := leading_parser termParser maxPrec >> declSig
|
||||
|
||||
private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax :=
|
||||
env.evalConstCheck Syntax opts ``Syntax constName
|
||||
|
||||
@[implemented_by evalSyntaxConstantUnsafe]
|
||||
private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
|
||||
|
||||
/-- Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`. -/
|
||||
partial def delabConstWithSignature : Delab := do
|
||||
let e ← getExpr
|
||||
-- use virtual expression node of arity 2 to separate name and type info
|
||||
let idStx ← descend e 0 <|
|
||||
withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
|
||||
delabConst
|
||||
descend (← inferType e) 1 <|
|
||||
delabParams idStx #[] #[]
|
||||
where
|
||||
-- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
|
||||
delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
|
||||
if let .forallE n d _ i ← getExpr then
|
||||
let stxN ← annotateCurPos (mkIdent n)
|
||||
let curIds := curIds.push ⟨stxN⟩
|
||||
if ← shouldGroupWithNext then
|
||||
withBindingBody n <| delabParams idStx groups curIds
|
||||
else
|
||||
let delabTy := withOptions (pp.piBinderTypes.set · true) delab
|
||||
let group ← withBindingDomain do
|
||||
match i with
|
||||
| .implicit => `(bracketedBinderF|{$curIds* : $(← delabTy)})
|
||||
| .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
|
||||
| .instImplicit => `(bracketedBinderF|[$curIds.back : $(← delabTy)])
|
||||
| _ =>
|
||||
if d.isOptParam then
|
||||
`(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
|
||||
else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
|
||||
let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
|
||||
`(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
|
||||
else
|
||||
`(bracketedBinderF|($curIds* : $(← delabTy)))
|
||||
withBindingBody n <| delabParams idStx (groups.push group) #[]
|
||||
else
|
||||
let type ← delab
|
||||
`(declSigWithId| $idStx:ident $groups* : $type)
|
||||
|
||||
end Lean.PrettyPrinter.Delaborator
|
||||
|
|
|
|||
|
|
@ -71,7 +71,7 @@ def handleHover (p : HoverParams)
|
|||
-- prefer info tree if at least as specific as parser docstring
|
||||
if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
|
||||
if let some hoverFmt ← i.fmtHover? ci then
|
||||
return mkHover (toString hoverFmt) range
|
||||
return mkHover (toString hoverFmt.fmt) range
|
||||
|
||||
if let some (doc, range) := stxDoc? then
|
||||
return mkHover doc range
|
||||
|
|
|
|||
|
|
@ -200,13 +200,15 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
|
|||
return none
|
||||
|
||||
/-- Construct a hover popup, if any, from an info node in a context.-/
|
||||
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
|
||||
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
|
||||
ci.runMetaM i.lctx do
|
||||
let mut fmts := #[]
|
||||
let mut infos := ∅
|
||||
let modFmt ← try
|
||||
let (termFmt, modFmt) ← fmtTermAndModule?
|
||||
if let some f := termFmt then
|
||||
fmts := fmts.push f
|
||||
fmts := fmts.push f.fmt
|
||||
infos := f.infos
|
||||
pure modFmt
|
||||
catch _ => pure none
|
||||
if let some m ← i.docString? then
|
||||
|
|
@ -216,14 +218,14 @@ def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
|
|||
if fmts.isEmpty then
|
||||
return none
|
||||
else
|
||||
return f!"\n***\n".joinSep fmts.toList
|
||||
return some ⟨f!"\n***\n".joinSep fmts.toList, infos⟩
|
||||
|
||||
where
|
||||
fmtModule? (decl : Name) : MetaM (Option Format) := do
|
||||
let some mod ← findModuleOf? decl | return none
|
||||
return some f!"*import {mod}*"
|
||||
|
||||
fmtTermAndModule? : MetaM (Option Format × Option Format) := do
|
||||
fmtTermAndModule? : MetaM (Option FormatWithInfos × Option Format) := do
|
||||
match i with
|
||||
| Info.ofTermInfo ti =>
|
||||
let e ← instantiateMVars ti.expr
|
||||
|
|
@ -232,20 +234,18 @@ where
|
|||
return (none, none)
|
||||
let tp ← instantiateMVars (← Meta.inferType e)
|
||||
let tpFmt ← Meta.ppExpr tp
|
||||
if e.isConst then
|
||||
-- Recall that `ppExpr` adds a `@` if the constant has implicit arguments, and it is quite distracting
|
||||
let eFmt ← withOptions (pp.fullNames.set · true |> (pp.universes.set · true)) <| PrettyPrinter.ppConst e
|
||||
return (some f!"```lean\n{eFmt} : {tpFmt}\n```", ← fmtModule? e.constName!)
|
||||
else
|
||||
let eFmt ← Meta.ppExpr e
|
||||
-- Try not to show too scary internals
|
||||
let showTerm := if let .fvar _ := e then
|
||||
if let some ldecl := (← getLCtx).findFVar? e then
|
||||
!ldecl.userName.hasMacroScopes
|
||||
else false
|
||||
else isAtomicFormat eFmt
|
||||
let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt
|
||||
return (some f!"```lean\n{fmt}\n```", none)
|
||||
if let .const c _ := e then
|
||||
let eFmt ← PrettyPrinter.ppSignature c
|
||||
return (some { eFmt with fmt := f!"```lean\n{eFmt.fmt}\n```" }, ← fmtModule? c)
|
||||
let eFmt ← Meta.ppExpr e
|
||||
-- Try not to show too scary internals
|
||||
let showTerm := if let .fvar _ := e then
|
||||
if let some ldecl := (← getLCtx).findFVar? e then
|
||||
!ldecl.userName.hasMacroScopes
|
||||
else false
|
||||
else isAtomicFormat eFmt
|
||||
let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt
|
||||
return (some f!"```lean\n{fmt}\n```", none)
|
||||
| Info.ofFieldInfo fi =>
|
||||
let tp ← Meta.inferType fi.val
|
||||
let tpFmt ← Meta.ppExpr tp
|
||||
|
|
|
|||
|
|
@ -2,10 +2,11 @@
|
|||
"position": {"line": 17, "character": 19}}
|
||||
{"range":
|
||||
{"start": {"line": 17, "character": 19}, "end": {"line": 17, "character": 20}},
|
||||
"contents": {"value": "```lean\nFoo.f : Nat → Bool\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value": "```lean\nFoo.f (n : Nat) : Bool\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://amb.lean"},
|
||||
"position": {"line": 19, "character": 19}}
|
||||
{"range":
|
||||
{"start": {"line": 19, "character": 19}, "end": {"line": 19, "character": 20}},
|
||||
"contents":
|
||||
{"value": "```lean\nBoo.f : String → String\n```", "kind": "markdown"}}
|
||||
{"value": "```lean\nBoo.f (n : String) : String\n```", "kind": "markdown"}}
|
||||
|
|
|
|||
|
|
@ -256,3 +256,6 @@ example : Nat :=
|
|||
let x := match 0 with | _ => 0
|
||||
_
|
||||
--^ textDocument/hover
|
||||
|
||||
def auto (o : Nat := by exact 1) : Nat := o
|
||||
--^ textDocument/hover
|
||||
|
|
|
|||
|
|
@ -120,7 +120,7 @@
|
|||
{"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.add (a✝a✝¹ : Nat) : Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 77, "character": 10}}
|
||||
|
|
@ -180,7 +180,7 @@
|
|||
"end": {"line": 102, "character": 31}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nLean.ParserDescr.sepBy1 (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr)\n (allowTrailingSep : Bool := false) : Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 102, "character": 31}}
|
||||
|
|
@ -212,7 +212,7 @@
|
|||
"end": {"line": 119, "character": 10}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nid.{u} {α : Sort u} (a : α) : α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 119, "character": 10}}
|
||||
|
|
@ -260,13 +260,13 @@
|
|||
{"start": {"line": 147, "character": 17},
|
||||
"end": {"line": 147, "character": 19}},
|
||||
"contents":
|
||||
{"value": "```lean\nBar.Foo.mk : ℕ → Foo\n```", "kind": "markdown"}}
|
||||
{"value": "```lean\nBar.Foo.mk (hi : ℕ) : Foo\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 150, "character": 2}}
|
||||
{"range":
|
||||
{"start": {"line": 150, "character": 2}, "end": {"line": 150, "character": 4}},
|
||||
"contents":
|
||||
{"value": "```lean\nBar.Foo.hi : Foo → ℕ\n```", "kind": "markdown"}}
|
||||
{"value": "```lean\nBar.Foo.hi (self : Foo) : ℕ\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 153, "character": 10}}
|
||||
{"range":
|
||||
|
|
@ -446,7 +446,7 @@ null
|
|||
{"start": {"line": 228, "character": 4}, "end": {"line": 228, "character": 8}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 228, "character": 9}}
|
||||
|
|
@ -511,7 +511,7 @@ null
|
|||
{"start": {"line": 247, "character": 4}, "end": {"line": 247, "character": 9}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 247, "character": 17}}
|
||||
|
|
@ -520,7 +520,7 @@ null
|
|||
"end": {"line": 247, "character": 20}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 250, "character": 27}}
|
||||
|
|
@ -529,7 +529,7 @@ null
|
|||
"end": {"line": 250, "character": 37}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nInhabited.mk.{1} : {α : Type} → α → Inhabited α\n```\n***\n*import Init.Prelude*",
|
||||
"```lean\nInhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α\n```\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 250, "character": 28}}
|
||||
|
|
@ -548,3 +548,10 @@ null
|
|||
{"value":
|
||||
"```lean\nlet x :=\n match 0 with\n | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hover.lean"},
|
||||
"position": {"line": 259, "character": 4}}
|
||||
{"range":
|
||||
{"start": {"line": 259, "character": 4}, "end": {"line": 259, "character": 8}},
|
||||
"contents":
|
||||
{"value": "```lean\nBar.auto (o : ℕ := by exact 1) : ℕ\n```",
|
||||
"kind": "markdown"}}
|
||||
|
|
|
|||
|
|
@ -4,5 +4,5 @@
|
|||
{"start": {"line": 8, "character": 17}, "end": {"line": 8, "character": 34}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nPalindrome.single.{u_1} : ∀ {α : Type u_1} (a : α), Palindrome [a]\n```",
|
||||
"```lean\nPalindrome.single.{u_1} {α : Type u_1} (a : α) : Palindrome [a]\n```",
|
||||
"kind": "markdown"}}
|
||||
|
|
|
|||
|
|
@ -12,51 +12,55 @@
|
|||
"position": {"line": 12, "character": 11}}
|
||||
{"range":
|
||||
{"start": {"line": 12, "character": 11}, "end": {"line": 12, "character": 13}},
|
||||
"contents": {"value": "```lean\nFoo.f₁ : Foo → Nat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value": "```lean\nFoo.f₁ (self : Foo) : Nat\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 12, "character": 14}}
|
||||
{"range":
|
||||
{"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 16, "character": 11}}
|
||||
{"range":
|
||||
{"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 13}},
|
||||
"contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 16, "character": 14}}
|
||||
{"range":
|
||||
{"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 19, "character": 13}}
|
||||
{"range":
|
||||
{"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 15}},
|
||||
"contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 19, "character": 16}}
|
||||
{"range":
|
||||
{"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 22, "character": 14}}
|
||||
{"range":
|
||||
{"start": {"line": 22, "character": 14}, "end": {"line": 22, "character": 16}},
|
||||
"contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
|
||||
"contents":
|
||||
{"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://hoverDot.lean"},
|
||||
"position": {"line": 22, "character": 17}}
|
||||
{"range":
|
||||
{"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
{"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
|
||||
"position": {"line": 0, "character": 52}}
|
||||
|
|
@ -17,7 +17,7 @@
|
|||
{"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
|
||||
"position": {"line": 7, "character": 54}}
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
{"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
|
||||
"position": {"line": 7, "character": 65}}
|
||||
|
|
@ -33,7 +33,7 @@
|
|||
{"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
{"textDocument": {"uri": "file://lean3HoverIssue.lean"},
|
||||
"position": {"line": 7, "character": 70}}
|
||||
|
|
@ -46,5 +46,5 @@
|
|||
{"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}},
|
||||
"contents":
|
||||
{"value":
|
||||
"```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
|
||||
"kind": "markdown"}}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue