Documentation

Lean.Level

def Nat.imax (n : Nat) (m : Nat) :
Equations
  • n.imax m = if m = 0 then 0 else n.max m
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
              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
                  @[reducible, inline]

                  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
                          Equations
                          • u.hash = u.data.hash
                          Instances For
                            Equations
                            • u.depth = u.data.depth.toNat
                            Instances For
                              Equations
                              • u.hasMVar = u.data.hasMVar
                              Instances For
                                Equations
                                • u.hasParam = u.data.hasParam
                                Instances For
                                  @[export lean_level_hash]
                                  Equations
                                  • u.hashEx = (hash u).toUInt32
                                  Instances For
                                    @[export lean_level_has_mvar]
                                    Equations
                                    Instances For
                                      @[export lean_level_has_param]
                                      Equations
                                      Instances For
                                        @[export lean_level_depth]
                                        Equations
                                        • u.depthEx = u.data.depth
                                        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
                                                                                  Instances For
                                                                                    Equations
                                                                                    • u.succ.getOffsetAux x = u.getOffsetAux (x + 1)
                                                                                    • x✝.getOffsetAux x = x
                                                                                    Instances For
                                                                                      Equations
                                                                                      • lvl.getOffset = lvl.getOffsetAux 0
                                                                                      Instances For
                                                                                        Equations
                                                                                        • a.succ.getLevelOffset = a.getLevelOffset
                                                                                        • x.getLevelOffset = x
                                                                                        Instances For
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[extern lean_level_eq]

                                                                                            occurs u l return true iff u occurs in l.

                                                                                            Equations
                                                                                            • x.occurs v₁.succ = (x == v₁.succ || x.occurs v₁)
                                                                                            • x.occurs (v₁.max v₂) = (x == v₁.max v₂ || x.occurs v₁ || x.occurs v₂)
                                                                                            • x.occurs (v₁.imax v₂) = (x == v₁.imax v₂ || x.occurs v₁ || x.occurs v₂)
                                                                                            • x✝.occurs x = (x✝ == x)
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[irreducible]
                                                                                                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
                                                                                                  • l₁.normLt l₂ = l₁.normLtAux 0 l₂ 0
                                                                                                  Instances For

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

                                                                                                    Equations
                                                                                                    • u.isEquiv v = (u == v || u.normalize == v.normalize)
                                                                                                    Instances For

                                                                                                      Reduce (if possible) universe level by 1

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            Equations
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              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
                                                                                                                  Instances For
                                                                                                                    @[implemented_by _private.Lean.Level.0.Lean.Level.updateMax!Impl]
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[implemented_by _private.Lean.Level.0.Lean.Level.updateIMax!Impl]
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[specialize #[]]
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            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
                                                                                                                                            • v.succ.collectMVars s = v.collectMVars s
                                                                                                                                            • (u_2.max v).collectMVars s = u_2.collectMVars (v.collectMVars s)
                                                                                                                                            • (u_2.imax v).collectMVars s = u_2.collectMVars (v.collectMVars s)
                                                                                                                                            • (Lean.Level.mvar n).collectMVars s = Lean.RBTree.insert s n
                                                                                                                                            • u.collectMVars s = s
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  Equations
                                                                                                                                                  • u.any p = (u.find? p).isSome
                                                                                                                                                  Instances For
                                                                                                                                                    @[reducible, inline]
                                                                                                                                                    abbrev Nat.toLevel (n : Nat) :
                                                                                                                                                    Equations
                                                                                                                                                    Instances For