Documentation

Lean.Level

def Nat.imax (n : Nat) (m : Nat) :
Equations
Instances For

    Cached hash code, cached results, and other data for Level. hash : 32-bits hasMVar : 1-bit hasParam : 1-bit depth : 24-bits

    Equations
    Instances For
      Equations
      def Lean.Level.mkData (h : UInt64) (depth : optParam Nat 0) (hasMVar : optParam Bool false) (hasParam : optParam Bool false) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.

        Universe level metavariable Id

        Instances For
          @[inline, reducible]

          Short for LevelMVarId

          Equations
          Instances For
            Equations
            Equations
            Instances For
              Equations
              Equations
              Instances For
                Equations
                instance Lean.instForInLMVarIdMapProdLMVarId {m : Type u_1 → Type u_2} {α : Type} :
                Equations
                Equations
                • Lean.instInhabitedLMVarIdMap = { default := }
                @[implemented_by Lean.Level.data._override]
                Equations
                Instances For
                  @[export lean_level_hash]
                  Equations
                  Instances For
                    @[export lean_level_has_mvar]
                    Equations
                    Instances For
                      @[export lean_level_has_param]
                      Equations
                      Instances For
                        @[export lean_level_depth]
                        Equations
                        Instances For
                          Equations
                          Instances For
                            @[export lean_level_mk_zero]
                            Equations
                            Instances For
                              @[export lean_level_mk_succ]
                              Equations
                              Instances For
                                @[export lean_level_mk_mvar]
                                Equations
                                Instances For
                                  @[export lean_level_mk_param]
                                  Equations
                                  Instances For
                                    @[export lean_level_mk_max]
                                    Equations
                                    Instances For
                                      @[export lean_level_mk_imax]
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                Equations
                                                Instances For
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          @[extern lean_level_eq]

                                                          occurs u l return true iff u occurs in l.

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

                                                              A total order on level expressions that has the following properties

                                                              • succ l is an immediate successor of l.
                                                              • zero is the minimal element. This total order is used in the normalization procedure.
                                                              Equations
                                                              Instances For

                                                                Return true if u and v denote the same level. Check is currently incomplete.

                                                                Equations
                                                                Instances For

                                                                  Reduce (if possible) universe level by 1

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

                                                                          The update functions try to avoid allocating new values using pointer equality. Note that if the update*! functions are used under a match-expression, the compiler will eliminate the double-match.

                                                                          @[implemented_by _private.Lean.Level.0.Lean.Level.updateSucc!Impl]
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  @[inline, reducible]
                                                                                  abbrev Lean.LevelMap (α : Type) :
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline, reducible]
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline, reducible]
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline, reducible]
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline, reducible]
                                                                                          Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline, reducible]
                                                                                              abbrev Nat.toLevel (n : Nat) :
                                                                                              Equations
                                                                                              Instances For