Documentation

Lean.Level

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

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

    Instances For
      def Lean.Level.mkData (h : UInt64) (depth : optParam Nat 0) (hasMVar : optParam Bool false) (hasParam : optParam Bool false) :
      Instances For

        Universe level metavariable Id

        Instances For
          @[inline, reducible]

          Short for LevelMVarId

          Instances For
            Instances For
              Instances For
                @[implemented_by Lean.Level.data._override]
                Equations
                Instances For
                  Instances For
                    Instances For
                      Instances For
                        Instances For
                          @[export lean_level_hash]
                          Instances For
                            @[export lean_level_has_mvar]
                            Instances For
                              @[export lean_level_has_param]
                              Instances For
                                @[export lean_level_depth]
                                Instances For
                                  Instances For
                                    Instances For
                                      @[export lean_level_mk_zero]
                                      Instances For
                                        @[export lean_level_mk_succ]
                                        Instances For
                                          @[export lean_level_mk_mvar]
                                          Instances For
                                            @[export lean_level_mk_param]
                                            Instances For
                                              @[export lean_level_mk_max]
                                              Instances For
                                                @[export lean_level_mk_imax]
                                                Instances For
                                                  Instances For
                                                    Instances For
                                                      Instances For
                                                        Instances For
                                                          @[extern lean_level_eq]

                                                          occurs u l return true iff u occurs in l.

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

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

                                                              Instances For

                                                                Reduce (if possible) universe level by 1

                                                                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]
                                                                  Instances For
                                                                    @[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
                                                                    Instances For
                                                                      @[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]
                                                                      Instances For
                                                                        @[specialize #[]]
                                                                        Instances For
                                                                          Equations
                                                                          Instances For
                                                                            Instances For
                                                                              @[inline, reducible]
                                                                              abbrev Lean.LevelMap (α : Type) :
                                                                              Instances For
                                                                                @[inline, reducible]
                                                                                Instances For
                                                                                  @[inline, reducible]
                                                                                  Instances For
                                                                                    @[inline, reducible]
                                                                                    Instances For
                                                                                      @[inline, reducible]
                                                                                      Instances For
                                                                                        Equations
                                                                                        Instances For
                                                                                          Instances For
                                                                                            @[inline, reducible]
                                                                                            abbrev Nat.toLevel (n : Nat) :
                                                                                            Instances For