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
        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) :
              Equations
              • One or more equations did not get rendered due to their size.

              Universe level metavariable Id

              Instances For
                Equations
                Instances For
                  @[reducible, inline]

                  Short for LevelMVarId

                  Equations
                  Instances For
                    Equations
                    Equations
                    Instances For
                      @[implemented_by Lean.Level.data._override]
                      noncomputable def Lean.Level.data :
                      Equations
                      Instances For
                        inductive Lean.Level :
                        Instances For
                          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
                                                      @[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

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

                                                                              Equations
                                                                              Instances For

                                                                                Returns true if and only if l evaluates to zero for all instantiations of parameters and meta-variables.

                                                                                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
                                                                                            @[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
                                                                                                      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
                                                                                                          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
                                                                                                                        @[specialize #[]]
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def Lean.Level.instantiateParams (u : Level) (paramNames : List Name) (vs : List Level) :
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              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
                                                                                                                                            def Lean.Level.any (u : Level) (p : LevelBool) :
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline]
                                                                                                                                              abbrev Nat.toLevel (n : Nat) :
                                                                                                                                              Equations
                                                                                                                                              Instances For