Documentation

Lake.Util.Name

@[inline]
Equations
  • Lake.NameMap.empty = Lean.RBMap.empty
Instances For
    instance Lake.instForInNameMapProdName {m : Type u_1 → Type u_2} {α : Type} :
    Equations
    Equations
    • Lake.instCoeRBMapNameQuickCmpNameMap = { coe := id }
    @[inline, reducible]
    abbrev Lake.OrdNameMap (α : Type u_1) :
    Type u_1
    Equations
    Instances For
      @[inline]
      Equations
      • Lake.OrdNameMap.empty = Lake.RBArray.empty
      Instances For
        @[inline]
        Equations
        Instances For
          @[inline, reducible]
          abbrev Lake.DNameMap (α : Lake.NameType u_1) :
          Type u_1
          Equations
          Instances For
            @[inline]
            Equations
            • Lake.DNameMap.empty = Lake.DRBMap.empty
            Instances For

              Name Helpers #

              @[simp]
              theorem Lake.Name.beq_false (m : Lake.Name) (n : Lake.Name) :
              (m == n) = false ¬m = n
              Equations
              Instances For