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

chore: remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-29 20:37:49 -07:00
parent f7d055830b
commit 3db5b7e4ca
1 changed files with 0 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Meta.lean
View file

@ -235,20 +235,6 @@ partial def getHead? : Syntax → Option Syntax
| node _ args => args.findSome? getHead?
| _ => none
partial def getHeadPos? (stx : Syntax) (originalOnly := false) : Option String.Pos := do
match stx, originalOnly with
| atom (SourceInfo.original (pos := pos) ..) val, _ => some pos
| atom (SourceInfo.synthetic (pos := pos) ..) _, false => some pos
| ident (SourceInfo.original (pos := pos) ..) val .., _ => some pos
| ident (SourceInfo.synthetic (pos := pos) ..) .., false => some pos
| node _ args, _ =>
for arg in args do
match getHeadPos? arg originalOnly with
| r@(some _) => return r
| _ => pure ()
return none
| _, _ => none
end Syntax
/-- Use the head atom/identifier of the current `ref` as the `ref` -/