Documentation

Lean.Level

def Nat.imax (n 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
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          @[extern lean_level_mk_data]
                          opaque Lean.Level.mkData (h : UInt64) (depth : Nat := 0) (hasMVar hasParam : Bool := false) :

                          Universe level metavariable Id

                          Instances For
                            @[reducible, inline]

                            Short for LevelMVarId

                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        instance Lean.instForInLMVarIdMapProdLMVarId {m : Type u_1 → Type u_2} {α : Type} :
                                        Equations
                                          inductive Lean.Level :
                                          Instances For
                                            @[implemented_by Lean.Level.data._override]
                                            noncomputable def Lean.Level.data :
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            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
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For
                                                                                            Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    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

                                                                                                                                                                    If result is true, then forall assignments A which assigns all parameters and metavariables occurring in l, l[A] != zero

                                                                                                                                                                    Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            Equations
                                                                                                                                                                              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]
                                                                                                                                                                                                          opaque Lean.Level.beq (a b : Level) :

                                                                                                                                                                                                          occurs u l return true iff u occurs in l.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[irreducible]
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def Lean.Level.normLt (l₁ l₂ : Level) :

                                                                                                                                                                                                                      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
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    def Lean.Level.format (u : Level) (mvars : Bool) :
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        def Lean.Level.quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) :
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    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]
                                                                                                                                                                                                                                                                              def Lean.Level.updateSucc! (lvl newLvl : Level) :
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  @[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
                                                                                                                                                                                                                                                                                  def Lean.Level.updateMax! (lvl newLhs newRhs : Level) :
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      @[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]
                                                                                                                                                                                                                                                                                      def Lean.Level.updateIMax! (lvl newLhs newRhs : Level) :
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              @[specialize #[]]
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          def Lean.Level.instantiateParams (u : Level) (paramNames : List Name) (vs : List Level) :
                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  @[irreducible]
                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                                                                                                                      abbrev Lean.LevelMap (α : Type) :
                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      def Lean.Level.any (u : Level) (p : LevelBool) :
                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                          abbrev Nat.toLevel (n : Nat) :
                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                            Instances For