| import Lean | |
| open Lean | |
| def oh_no : Nat := 0 | |
| def snakeLinter : Linter where | |
| run stx := do | |
| if stx.getKind == ``Lean.Parser.Command.declaration then | |
| let decl := stx[1] | |
| if decl.getKind == ``Lean.Parser.Command.definition then | |
| let declId := decl[1] | |
| withRef declId do | |
| let declName := declId[0].getId | |
| if declName.eraseMacroScopes.toString.contains '_' then | |
| -- TODO(Sebastian): return actual message with position from syntax tree | |
| throwError "SNAKES!!" | |
| initialize addLinter snakeLinter |