fpvandoorn

/-
Copyright (c) 2022 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/

import Mathlib.Init.Data.Nat.Notation
import Mathlib.Lean.Message
import Mathlib.Lean.Expr.Basic
import Mathlib.Data.String.Defs

fpvandoorn

import Mathlib.Init.Data.Nat.Notation
import Mathlib.Lean.Message
import Mathlib.Lean.Expr.Basic
import Mathlib.Data.String.Defs
import Mathlib.Tactic.Simps.NotationClass

open Lean Elab Parser Command
open Meta hiding Config
open Elab.Term hiding mkConst

fpvandoorn

def read (s : String) : List (Option (Nat ⊕ Nat)) :=
s.data.map fun
| '(' => .some <| .inl 0
| '{' => .some <| .inl 1
| '[' => .some <| .inl 2
| '<' => .some <| .inl 3
| ')' => .some <| .inr 0
| '}' => .some <| .inr 1
| ']' => .some <| .inr 2
| '>' => .some <| .inr 3

fpvandoorn

import Mathlib.Tactic.LibrarySearch
import Mathlib.Tactic.Propose

open Lean Elab Server Lsp RequestM Parser Mathlib Tactic LibrarySearch Meta Std.Tactic.TryThis
  Propose

structure TryThisInfo where
  replacement : Syntax
  deriving TypeName

fpvandoorn

import Mathlib

open Lean Meta Elab Command

-- generalized
/-- Write an import graph, represented as a an array of `NameMap`s to the ".dot" graph format.
  If `("style1", graph1)` is in `graphs`, then the edges in `graph1` will be labeled with `[style1]`.
  Example: `asStyledDotGraph #[("", graph1), ("style=dashed", graph2)]` -/
def asStyledDotGraph [ForIn Id α Name] (graphs : Array (String × NameMap α))
    (header := "import_graph") : String := Id.run do