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

def Lean.Parser.Category.sym_dsimproc : Category

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

Do nothing

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

Evaluate ground (fully concrete) terms.

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

Beta reduction

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

zeta reduction. That is, expands let-expressions.

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

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

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

Projection reduction.

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

match-expression reduction.

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

Apply a, then apply b to the result.

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

Try a, if no progress try b.

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

Parenthesized dsimproc expression.

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

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

def Lean.Parser.Command.symDSimpFieldPre : ParserDescr

Pre-processing simproc chain.

def Lean.Parser.Command.symDSimpFieldPost : ParserDescr

Post-processing simproc chain.

def Lean.Parser.Command.symDSimpFieldMaxSteps : ParserDescr

Maximum number of simplification steps.

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