def Array.reduceGetElem : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n] for n a Nat literal.

Equations

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

def Array.reduceGetElem? : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n]? for n a Nat literal.

Equations

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

def Array.reduceGetElem! : Lean.Meta.Simp.DSimproc

Simplification procedure for #[...][n]! for n a Nat literal.

Equations

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