structure RebindDescr : Type

• fnName : Lean.Name
• type : Lean.Expr
• impl? : Option Lean.Name

instance instInhabitedRebindDescr : Inhabited RebindDescr

Equations

• instInhabitedRebindDescr = { default := { fnName := default, type := default, impl? := default } }

@[reducible, inline]

abbrev RebindState : Type

Equations

• RebindState = Lean.NameMap RebindDescr

@[reducible, inline]

abbrev RebindExtension : Type

Equations

• RebindExtension = Lean.SimpleScopedEnvExtension RebindDescr RebindState

def RebindState.addEntry (s : Lean.NameMap RebindDescr) (r : RebindDescr) : Lean.NameMap RebindDescr

Equations

• RebindState.addEntry s r = s.insert r.fnName r

opaque rebindExtension : RebindExtension

def getRebinds (env : Lean.Environment) : Lean.NameMap RebindDescr

Equations

• getRebinds env = Lean.ScopedEnvExtension.getState rebindExtension env

def getRebind? (env : Lean.Environment) (fnName : Lean.Name) : Option RebindDescr

Equations

• getRebind? env fnName = (getRebinds env).find? fnName

def rebindAttr : Lean.ParserDescr

Equations

• rebindAttr = Lean.ParserDescr.node `rebindAttr 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rebind " false) (Lean.ParserDescr.const `ident))

unsafe def RebindExtension.evalUnsafe {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) [Inhabited (m α)] (n : Lean.Name) : m α

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by RebindExtension.evalUnsafe]

opaque RebindExtension.eval {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (α : Type) [Inhabited (m α)] (n : Lean.Name) : m α

def «commandDeclare_rebindable_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def evalRebindStx : Lean.ParserDescr

Equations

• evalRebindStx = Lean.ParserDescr.node `evalRebindStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval_rebind% ") (Lean.ParserDescr.const `ident))

def elabEvalRebindStx : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.