- missing: Aesop.SyntaxMap.Key
- node: Lean.SyntaxNodeKind → Aesop.SyntaxMap.Key
- atom: String → Aesop.SyntaxMap.Key
- ident: Lean.Name → Aesop.SyntaxMap.Key
Instances For
Equations
- Aesop.SyntaxMap.instInhabitedKey = { default := Aesop.SyntaxMap.Key.missing }
Equations
- Aesop.SyntaxMap.instBEqKey = { beq := Aesop.SyntaxMap.beqKey✝ }
Equations
- Aesop.SyntaxMap.instHashableKey = { hash := Aesop.SyntaxMap.hashKey✝ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- toPHashMap : Lean.PHashMap Aesop.SyntaxMap.Key α
Instances For
Equations
- Aesop.instInhabitedSyntaxMap = { default := { toPHashMap := default } }
- keys : Array Aesop.SyntaxMap.Key
- run : Lean.Syntax → Lean.CoreM (Option Lean.Syntax)
Instances For
Equations
- Aesop.instInhabitedSyntaxRewrite = { default := { keys := default, run := default } }
Equations
- Aesop.SyntaxMap.empty = { toPHashMap := Lean.PersistentHashMap.empty }
Instances For
Equations
- Aesop.SyntaxMap.instEmptyCollection = { emptyCollection := Aesop.SyntaxMap.empty }
def
Aesop.SyntaxMap.find?
{α : Type u_1}
(key : Aesop.SyntaxMap.Key)
(m : Aesop.SyntaxMap α)
:
Option α
Equations
- Aesop.SyntaxMap.find? key m = Lean.PersistentHashMap.find? m.toPHashMap key
Instances For
Equations
Instances For
def
Aesop.SyntaxMap.insert
{α : Type u_1}
(key : Aesop.SyntaxMap.Key)
(val : α)
(m : Aesop.SyntaxMap α)
:
Equations
- Aesop.SyntaxMap.insert key val m = { toPHashMap := Lean.PersistentHashMap.insert m.toPHashMap key val }
Instances For
@[macro_inline]
def
Aesop.SyntaxMap.insertWith
{α : Type u_1}
(key : Aesop.SyntaxMap.Key)
(a : α)
(f : α → α)
(m : Aesop.SyntaxMap α)
:
Equations
- Aesop.SyntaxMap.insertWith key a f m = match Aesop.SyntaxMap.find? key m with | some a' => Aesop.SyntaxMap.insert key (f a') m | none => Aesop.SyntaxMap.insert key a m
Instances For
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Aesop.optimizeSyntaxWith rws stx = Aesop.optimizeSyntaxWith.go rws stx
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.optimizeSyntax
{kind : Lean.SyntaxNodeKinds}
(stx : Lean.TSyntax kind)
:
Lean.CoreM (Lean.TSyntax kind)
Equations
- One or more equations did not get rendered due to their size.