DSimproc DSL for Sym.dsimp

A syntax category for specifying pre and post dsimproc chains in Sym.dsimp variants.

Primitives

• ground — evaluates ground (fully concrete) terms
• beta — beta reduction
• zeta - zeta reduction
• zeta_delta [ids] - zeta delta reduction
• proj - reduce projections
• match - reduce match-expressions

Combinators

• a >> b — apply a, then apply b to the result (andThen)
• a <|> b — try a, if no progress try b (orElse)

def Lean.Parser.Sym.DSimp.sym_dsimproc.quot : ParserDescr

Equations

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

def Lean.Parser.Category.sym_dsimproc : Category

Equations

• Lean.Parser.Category.sym_dsimproc = { }

def Lean.Parser.Sym.DSimp.none : ParserDescr

Do nothing

Equations

• Lean.Parser.Sym.DSimp.none = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.none 1024 (Lean.ParserDescr.nonReservedSymbol "none" false)

def Lean.Parser.Sym.DSimp.ground : ParserDescr

Evaluate ground (fully concrete) terms.

Equations

• Lean.Parser.Sym.DSimp.ground = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.ground 1024 (Lean.ParserDescr.nonReservedSymbol "ground" false)

def Lean.Parser.Sym.DSimp.beta : ParserDescr

Beta reduction

Equations

• Lean.Parser.Sym.DSimp.beta = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.beta 1024 (Lean.ParserDescr.nonReservedSymbol "beta" false)

def Lean.Parser.Sym.DSimp.zeta : ParserDescr

zeta reduction. That is, expands let-expressions.

Equations

• Lean.Parser.Sym.DSimp.zeta = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.zeta 1024 (Lean.ParserDescr.nonReservedSymbol "zeta" false)

def Lean.Parser.Sym.DSimp.zetaDelta : ParserDescr

zeta delta reduction. That is, expands all let-declarations.

Equations

• Lean.Parser.Sym.DSimp.zetaDelta = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.zetaDelta 1024 (Lean.ParserDescr.nonReservedSymbol "zeta_delta" false)

def Lean.Parser.Sym.DSimp.proj : ParserDescr

Projection reduction.

Equations

• Lean.Parser.Sym.DSimp.proj = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.proj 1024 (Lean.ParserDescr.nonReservedSymbol "proj" false)

def Lean.Parser.Sym.DSimp.reduceMatch : ParserDescr

match-expression reduction.

Equations

• Lean.Parser.Sym.DSimp.reduceMatch = Lean.ParserDescr.node `Lean.Parser.Sym.DSimp.reduceMatch 1024 (Lean.ParserDescr.nonReservedSymbol "match" false)

def Lean.Parser.Sym.DSimp.andThen : TrailingParserDescr

Apply a, then apply b to the result.

Equations

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

def Lean.Parser.Sym.DSimp.orElse : TrailingParserDescr

Try a, if no progress try b.

Equations

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

def Lean.Parser.Sym.DSimp.dsimprocParen : ParserDescr

Parenthesized dsimproc expression.

Equations

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

register_sym_dsimp command

Declares a named Sym.dsimp variant with pre/post simproc chains and optional config overrides.

register_sym_dsimp myVariant where
  pre  := match
  post := ground >> zeta_delta

def Lean.Parser.Category.sym_dsimp_field : Category

Equations

• Lean.Parser.Category.sym_dsimp_field = { }

def Lean.Parser.Command.sym_dsimp_field.quot : ParserDescr

Equations

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

def Lean.Parser.Command.symDSimpFieldPre : ParserDescr

Pre-processing simproc chain.

Equations

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

def Lean.Parser.Command.symDSimpFieldPost : ParserDescr

Post-processing simproc chain.

Equations

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

def Lean.Parser.Command.symDSimpFieldMaxSteps : ParserDescr

Maximum number of simplification steps.

Equations

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

def Lean.Parser.Command.registerSymDSimp : ParserDescr

Register a named Sym.dsimp variant.

register_sym_dsimp myVariant where
  pre  := match
  post := ground >> zeta_delta
  maxSteps := 50000

Equations

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