def DY.Step.stepArgs : Lean.ParserDescr

Equations

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

def DY.Step.nonMono (α : Sort u) : Sort u

Equations

• DY.Step.nonMono α = α

theorem DY.Step.makeNonMono {p : Prop} (h : p) : nonMono p

def DY.Step.make_non_monotone : Lean.ParserDescr

Equations

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

def DY.Step.step : Lean.ParserDescr

Equations

• DY.Step.step = Lean.ParserDescr.node `DY.Step.step 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "step" false) DY.Step.stepArgs)

def DY.Step.step_let : Lean.ParserDescr

Equations

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