Documentation

Lake.Util.Name

@[inline]
Instances For
    instance Lake.instForInNameMapProdName {m : Type u_1 → Type u_2} {α : Type} :
    @[inline, reducible]
    abbrev Lake.OrdNameMap (α : Type u_1) :
    Type u_1
    Instances For
      @[inline]
      Instances For
        @[inline]
        Instances For
          @[inline, reducible]
          abbrev Lake.DNameMap (α : Lake.NameType u_1) :
          Type u_1
          Instances For
            @[inline]
            Instances For

              Name Helpers #

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