Lean.Level

Lean.Level.mvarId! x = match x with | Lean.Level.mvar mvarId x => mvarId | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.mvarId!" 189 21 "metavariable expected"

source

def Lean.Level.isNeverZero :

Lean.Level → Bool

Equations

Lean.Level.isNeverZero (Lean.Level.zero x_1) = false
Lean.Level.isNeverZero (Lean.Level.param x_1 x_2) = false
Lean.Level.isNeverZero (Lean.Level.mvar x_1 x_2) = false
Lean.Level.isNeverZero (Lean.Level.succ x_1 x_2) = true
Lean.Level.isNeverZero (Lean.Level.max l₁ l₂ x_1) = (Lean.Level.isNeverZero l₁ || Lean.Level.isNeverZero l₂)
Lean.Level.isNeverZero (Lean.Level.imax l₁ l₂ x_1) = Lean.Level.isNeverZero l₂

source

def Lean.Level.ofNat :

Nat → Lean.Level

Equations

Lean.Level.ofNat 0 = Lean.levelZero
Lean.Level.ofNat (Nat.succ n) = Lean.mkLevelSucc (Lean.Level.ofNat n)

source

def Lean.Level.addOffsetAux :

Nat → Lean.Level → Lean.Level

Equations

Lean.Level.addOffsetAux 0 x = x
Lean.Level.addOffsetAux (Nat.succ n) x = Lean.Level.addOffsetAux n (Lean.mkLevelSucc x)

source

def Lean.Level.addOffset (u : Lean.Level) (n : Nat) :

Lean.Level

Equations

Lean.Level.addOffset u n = Lean.Level.addOffsetAux n u

source

def Lean.Level.isExplicit :

Lean.Level → Bool

Equations

Lean.Level.isExplicit (Lean.Level.zero x_1) = true
Lean.Level.isExplicit (Lean.Level.succ u x_1) = (!Lean.Level.hasMVar u && !Lean.Level.hasParam u && Lean.Level.isExplicit u)
Lean.Level.isExplicit x = false

source

def Lean.Level.getOffsetAux :

Lean.Level → Nat → Nat

Equations

Lean.Level.getOffsetAux (Lean.Level.succ u x_2) x = Lean.Level.getOffsetAux u (x + 1)
Lean.Level.getOffsetAux x x = x

source

def Lean.Level.getOffset (lvl : Lean.Level) :

Nat

Equations

Lean.Level.getOffset lvl = Lean.Level.getOffsetAux lvl 0

source

def Lean.Level.getLevelOffset :

Lean.Level → Lean.Level

Equations

Lean.Level.getLevelOffset (Lean.Level.succ x_1 x_2) = Lean.Level.getLevelOffset x_1
Lean.Level.getLevelOffset x = x

source

def Lean.Level.toNat (lvl : Lean.Level) :

Option Nat

Equations

Lean.Level.toNat lvl = match Lean.Level.getLevelOffset lvl with | Lean.Level.zero x => some (Lean.Level.getOffset lvl) | x => none

source

@[extern lean_level_eq]

constant Lean.Level.beq (a : Lean.Level) (b : Lean.Level) :

Bool

source

instance Lean.Level.instBEqLevel :

BEq Lean.Level

Equations

Lean.Level.instBEqLevel = { beq := Lean.Level.beq }

source

def Lean.Level.occurs :

Lean.Level → Lean.Level → Bool

Equations

Lean.Level.occurs x (Lean.Level.succ v₁ x_2) = (x == Lean.Level.succ v₁ x_2 || Lean.Level.occurs x v₁)
Lean.Level.occurs x (Lean.Level.max v₁ v₂ x_2) = (x == Lean.Level.max v₁ v₂ x_2 || Lean.Level.occurs x v₁ || Lean.Level.occurs x v₂)
Lean.Level.occurs x (Lean.Level.imax v₁ v₂ x_2) = (x == Lean.Level.imax v₁ v₂ x_2 || Lean.Level.occurs x v₁ || Lean.Level.occurs x v₂)
Lean.Level.occurs x x = (x == x)

source

def Lean.Level.ctorToNat :

Lean.Level → Nat

Equations

Lean.Level.ctorToNat x = match x with | Lean.Level.zero x => 0 | Lean.Level.param x x_1 => 1 | Lean.Level.mvar x x_1 => 2 | Lean.Level.succ x x_1 => 3 | Lean.Level.max x x_1 x_2 => 4 | Lean.Level.imax x x_1 x_2 => 5

source

partial def Lean.Level.normLtAux :

Lean.Level → Nat → Lean.Level → Nat → Bool

source

def Lean.Level.normLt (l₁ : Lean.Level) (l₂ : Lean.Level) :

Bool

Equations

Lean.Level.normLt l₁ l₂ = Lean.Level.normLtAux l₁ 0 l₂ 0

source

partial def Lean.Level.normalize (l : Lean.Level) :

Lean.Level

source

def Lean.Level.isEquiv (u : Lean.Level) (v : Lean.Level) :

Bool

Equations

Lean.Level.isEquiv u v = (u == v || Lean.Level.normalize u == Lean.Level.normalize v)

source

def Lean.Level.dec :

Lean.Level → Option Lean.Level

Equations

Lean.Level.dec (Lean.Level.zero x_1) = none
Lean.Level.dec (Lean.Level.param x_1 x_2) = none
Lean.Level.dec (Lean.Level.mvar x_1 x_2) = none
Lean.Level.dec (Lean.Level.succ x_1 x_2) = some x_1
Lean.Level.dec (Lean.Level.max l₁ l₂ x_1) = OptionM.run do let a ← Lean.Level.dec l₁ let a_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax a a_1)
Lean.Level.dec (Lean.Level.imax l₁ l₂ x_1) = OptionM.run do let a ← Lean.Level.dec l₁ let a_1 ← Lean.Level.dec l₂ pure (Lean.mkLevelMax a a_1)

source

inductive Lean.Level.PP.Result :

Type

leaf: Lean.Name → Lean.Level.PP.Result
num: Nat → Lean.Level.PP.Result
offset: Lean.Level.PP.Result → Nat → Lean.Level.PP.Result
maxNode: List Lean.Level.PP.Result → Lean.Level.PP.Result
imaxNode: List Lean.Level.PP.Result → Lean.Level.PP.Result

source

def Lean.Level.PP.Result.succ :

Lean.Level.PP.Result → Lean.Level.PP.Result

Equations

Lean.Level.PP.Result.succ x = match x with | Lean.Level.PP.Result.offset f k => Lean.Level.PP.Result.offset f (k + 1) | Lean.Level.PP.Result.num k => Lean.Level.PP.Result.num (k + 1) | f => Lean.Level.PP.Result.offset f 1

source

def Lean.Level.PP.Result.max :

Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

Equations

Lean.Level.PP.Result.max x x = match x, x with | f, Lean.Level.PP.Result.maxNode Fs => Lean.Level.PP.Result.maxNode (f :: Fs) | f₁, f₂ => Lean.Level.PP.Result.maxNode [f₁, f₂]

source

def Lean.Level.PP.Result.imax :

Lean.Level.PP.Result → Lean.Level.PP.Result → Lean.Level.PP.Result

Equations

Lean.Level.PP.Result.imax x x = match x, x with | f, Lean.Level.PP.Result.imaxNode Fs => Lean.Level.PP.Result.imaxNode (f :: Fs) | f₁, f₂ => Lean.Level.PP.Result.imaxNode [f₁, f₂]

source

def Lean.Level.PP.toResult :

Lean.Level → Lean.Level.PP.Result

Equations

Lean.Level.PP.toResult (Lean.Level.zero a) = Lean.Level.PP.Result.num 0
Lean.Level.PP.toResult (Lean.Level.succ a a_1) = Lean.Level.PP.Result.succ (Lean.Level.PP.toResult a)
Lean.Level.PP.toResult (Lean.Level.max a a_1 a_2) = Lean.Level.PP.Result.max (Lean.Level.PP.toResult a) (Lean.Level.PP.toResult a_1)
Lean.Level.PP.toResult (Lean.Level.imax a a_1 a_2) = Lean.Level.PP.Result.imax (Lean.Level.PP.toResult a) (Lean.Level.PP.toResult a_1)
Lean.Level.PP.toResult (Lean.Level.param a a_1) = Lean.Level.PP.Result.leaf a
Lean.Level.PP.toResult (Lean.Level.mvar a a_1) = let n := Lean.Name.replacePrefix a.name `_uniq (Lean.Name.mkSimple "?u"); Lean.Level.PP.Result.leaf n

source

partial def Lean.Level.PP.Result.format :

Lean.Level.PP.Result → Bool → Lean.Format

source

partial def Lean.Level.PP.Result.quote (r : Lean.Level.PP.Result) (prec : Nat) :

Lean.Syntax

source

def Lean.Level.format (u : Lean.Level) :

Lean.Format

Equations

Lean.Level.format u = Lean.Level.PP.Result.format (Lean.Level.PP.toResult u) true

source

instance Lean.Level.instToFormatLevel :

Lean.ToFormat Lean.Level

Equations

Lean.Level.instToFormatLevel = { format := fun u => Lean.Level.format u }

source

instance Lean.Level.instToStringLevel :

ToString Lean.Level

Equations

Lean.Level.instToStringLevel = { toString := fun u => Lean.Format.pretty (Lean.Level.format u) }

source

def Lean.Level.quote (u : Lean.Level) (prec : optParam Nat 0) :

Lean.Syntax

Equations

Lean.Level.quote u prec = Lean.Level.PP.Result.quote (Lean.Level.PP.toResult u) prec

source

instance Lean.Level.instQuoteLevel :

Lean.Quote Lean.Level

Equations

Lean.Level.instQuoteLevel = { quote := fun u => Lean.Level.quote u }

source

def Lean.mkLevelMax' (u : Lean.Level) (v : Lean.Level) :

Lean.Level

Equations

Lean.mkLevelMax' u v = let subsumes := fun u v => if (Lean.Level.isExplicit v && decide (Lean.Level.getOffset u ≥ Lean.Level.getOffset v)) = true then true else match u with | Lean.Level.max u₁ u₂ x => v == u₁ || v == u₂ | x => false; if (u == v) = true then u else if Lean.Level.isZero u = true then v else if Lean.Level.isZero v = true then u else if subsumes u v = true then u else if subsumes v u = true then v else if (Lean.Level.getLevelOffset u == Lean.Level.getLevelOffset v) = true then if Lean.Level.getOffset u ≥ Lean.Level.getOffset v then u else v else Lean.mkLevelMax u v

source

def Lean.mkLevelIMax' (u : Lean.Level) (v : Lean.Level) :

Lean.Level

Equations

Lean.mkLevelIMax' u v = if Lean.Level.isNeverZero v = true then Lean.mkLevelMax' u v else if Lean.Level.isZero v = true then v else if Lean.Level.isZero u = true then v else if (u == v) = true then u else Lean.mkLevelIMax u v

source

@[extern lean_level_update_succ]

def Lean.Level.updateSucc (lvl : Lean.Level) (newLvl : Lean.Level) (h : Lean.Level.isSucc lvl = true) :

Lean.Level

Equations

Lean.Level.updateSucc lvl newLvl h = Lean.mkLevelSucc newLvl

source

@[inline]

def Lean.Level.updateSucc! (lvl : Lean.Level) (newLvl : Lean.Level) :

Lean.Level

Equations

Lean.Level.updateSucc! lvl newLvl = match lvl with | Lean.Level.succ lvl d => Lean.Level.updateSucc (Lean.Level.succ lvl d) newLvl (_ : Lean.Level.isSucc (Lean.Level.succ lvl d) = Lean.Level.isSucc (Lean.Level.succ lvl d)) | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.updateSucc!" 519 18 "succ level expected"

source

@[extern lean_level_update_max]

def Lean.Level.updateMax (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) (h : Lean.Level.isMax lvl = true) :

Lean.Level

Equations

Lean.Level.updateMax lvl newLhs newRhs h = Lean.mkLevelMax' newLhs newRhs

source

@[inline]

def Lean.Level.updateMax! (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) :

Lean.Level

Equations

Lean.Level.updateMax! lvl newLhs newRhs = match lvl with | Lean.Level.max lhs rhs d => Lean.Level.updateMax (Lean.Level.max lhs rhs d) newLhs newRhs (_ : Lean.Level.isMax (Lean.Level.max lhs rhs d) = Lean.Level.isMax (Lean.Level.max lhs rhs d)) | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.updateMax!" 528 21 "max level expected"

source

@[extern lean_level_update_imax]

def Lean.Level.updateIMax (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) (h : Lean.Level.isIMax lvl = true) :

Lean.Level

Equations

Lean.Level.updateIMax lvl newLhs newRhs h = Lean.mkLevelIMax' newLhs newRhs

source

@[inline]

def Lean.Level.updateIMax! (lvl : Lean.Level) (newLhs : Lean.Level) (newRhs : Lean.Level) :

Lean.Level

Equations

Lean.Level.updateIMax! lvl newLhs newRhs = match lvl with | Lean.Level.imax lhs rhs d => Lean.Level.updateIMax (Lean.Level.imax lhs rhs d) newLhs newRhs (_ : Lean.Level.isIMax (Lean.Level.imax lhs rhs d) = Lean.Level.isIMax (Lean.Level.imax lhs rhs d)) | x => panicWithPosWithDecl "Lean.Level" "Lean.Level.updateIMax!" 537 22 "imax level expected"

source

def Lean.Level.mkNaryMax :

List Lean.Level → Lean.Level

Equations

Lean.Level.mkNaryMax [] = Lean.levelZero
Lean.Level.mkNaryMax [u] = u
Lean.Level.mkNaryMax (u :: us) = Lean.mkLevelMax' u (Lean.Level.mkNaryMax us)

source

@[specialize]

def Lean.Level.instantiateParams (s : Lean.Name → Option Lean.Level) :

Lean.Level → Lean.Level

source

@[inline]

abbrev Lean.LevelMap (α : Type) :

Type

Equations

Lean.LevelMap α = Std.HashMap Lean.Level α

source

@[inline]

abbrev Lean.PersistentLevelMap (α : Type) :

Type

Equations

Lean.PersistentLevelMap α = Std.PHashMap Lean.Level α

source

@[inline]

abbrev Lean.LevelSet :

Type

Equations

Lean.LevelSet = Std.HashSet Lean.Level

source

@[inline]

abbrev Lean.PersistentLevelSet :

Type

Equations

Lean.PersistentLevelSet = Std.PHashSet Lean.Level

source

@[inline]

abbrev Lean.PLevelSet :

Type

Equations

Lean.PLevelSet = Lean.PersistentLevelSet

source

def Lean.Level.collectMVars (u : Lean.Level) (s : optParam Lean.MVarIdSet ∅) :

Lean.MVarIdSet

Equations

Lean.Level.collectMVars (Lean.Level.succ v x) s = Lean.Level.collectMVars v s
Lean.Level.collectMVars (Lean.Level.max u_2 v x) s = Lean.Level.collectMVars u_2 (Lean.Level.collectMVars v s)
Lean.Level.collectMVars (Lean.Level.imax u_2 v x) s = Lean.Level.collectMVars u_2 (Lean.Level.collectMVars v s)
Lean.Level.collectMVars (Lean.Level.mvar n x) s = Std.RBTree.insert s n
Lean.Level.collectMVars u s = s

source

def Lean.Level.find? (u : Lean.Level) (p : Lean.Level → Bool) :

Option Lean.Level

Equations

Lean.Level.find? u p = (fun visit => visit u) (Lean.Level.find?.visit p)

source

def Lean.Level.find?.visit (p : Lean.Level → Bool) (u : Lean.Level) :

OptionM Lean.Level

Equations

Lean.Level.find?.visit p (Lean.Level.succ v x) = if p (Lean.Level.succ v x) = true then pure (Lean.Level.succ v x) else Lean.Level.find?.visit p v
Lean.Level.find?.visit p (Lean.Level.max u_2 v x) = if p (Lean.Level.max u_2 v x) = true then pure (Lean.Level.max u_2 v x) else HOrElse.hOrElse (Lean.Level.find?.visit p u_2) fun x => Lean.Level.find?.visit p v
Lean.Level.find?.visit p (Lean.Level.imax u_2 v x) = if p (Lean.Level.imax u_2 v x) = true then pure (Lean.Level.imax u_2 v x) else HOrElse.hOrElse (Lean.Level.find?.visit p u_2) fun x => Lean.Level.find?.visit p v
Lean.Level.find?.visit p u = if p u = true then pure u else failure

source

def Lean.Level.any (u : Lean.Level) (p : Lean.Level → Bool) :

Bool

Equations

Lean.Level.any u p = Option.isSome (Lean.Level.find? u p)

source

@[inline]

abbrev Nat.toLevel (n : Nat) :

Lean.Level

Equations

Nat.toLevel n = Lean.Level.ofNat n