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

fix: code

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-12 19:11:21 -07:00
parent 1de3efff9d
commit 42436254ee
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Conv.lean
View file

@ -30,7 +30,6 @@ syntax (name := change) "change " term : conv
syntax (name := delta) "delta " ident : conv
syntax (name := pattern) "pattern " term : conv
syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
syntax (name := erewrite) "erewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := simpMatch) "simpMatch " : conv
@ -43,8 +42,9 @@ syntax (name := paren) "(" convSeq ")" : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
macro "erw " s:rwRuleSeq : conv => `(erewrite $s:rwRuleSeq)
macro "rw " c:(config)? s:rwRuleSeq : conv =>
let c? := if c.isNone then none else some c[0]
`(conv| rewrite $[$c?:config]? $s:rwRuleSeq)
macro "args" : conv => `(congr)
macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)

10
src/Lean/Server/FileWorker/RequestHandling.lean
View file

@ -59,7 +59,7 @@ partial def handleHover (p : HoverParams)
inductive GoToKind
| declaration | definition | type
deriving DecidableEq
deriving BEq
open Elab GoToKind in
partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
@ -112,7 +112,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
if let some (ci, i) := t.hoverableInfoAt? hoverPos then
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if kind = type then
if kind == type then
expr ← ci.runMetaM i.lctx do
Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
match expr with
@ -120,7 +120,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
| Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder t i id
| _ => pure ()
if let Info.ofFieldInfo fi := i then
if kind = type then
if kind == type then
let expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType fi.val)
if let some n := expr.getAppFn.constName? then
@ -129,9 +129,9 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? then
if kind = declaration ∧ ci.env.contains ei.stx.getKind then
if kind == declaration && ci.env.contains ei.stx.getKind then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
if kind = definition ∧ ci.env.contains ei.elaborator then
if kind == definition && ci.env.contains ei.elaborator then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
return #[]