Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array

source
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.
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For