Documentation

Init.Data.AC

structure Lean.Data.AC.Variable {α : Sort u} (op : ααα) :
Instances For
    structure Lean.Data.AC.Context (α : Sort u) :
    Instances For
      class Lean.Data.AC.ContextInformation (α : Sort u) :
      Sort (max 1 u)
      Instances
        class Lean.Data.AC.EvalInformation (α : Sort u) (β : Sort v) :
        Sort (max (max 1 u) v)
        • arbitrary : αβ
        • evalOp : αβββ
        • evalVar : αNatβ
        Instances
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            Instances For
              Equations
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Lean.Data.AC.List.two_step_induction {motive : List NatSort u} (l : List Nat) (empty : motive []) (single : (a : Nat) → motive [a]) (step : (a b : Nat) → (l : List Nat) → motive (b :: l)motive (a :: b :: l)) :
                      motive l
                      theorem Lean.Data.AC.Context.evalList_sort_congr {α : Sort u_1} {a : List Nat} {b : List Nat} {c : List Nat} (ctx : Lean.Data.AC.Context α) (h : Std.Commutative ctx.op) (h₂ : Lean.Data.AC.evalList α ctx a = Lean.Data.AC.evalList α ctx b) (h₃ : a []) (h₄ : b []) :
                      theorem Lean.Data.AC.Context.evalList_append {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (l : List Nat) (r : List Nat) (h₁ : l []) (h₂ : r []) :