Prelude: universe polymorphic basic types

Parsers in Type u return results in Type u, so combinators that would return Unit, Bool or Nat return Unitᵤ, Boolᵤ or Natᵤ instead. These coerce to Bool and Nat, and their Repr instances print the same as Bool and Nat.

@[reducible, inline]

abbrev ParseIt.Unitᵤ : Type u

Unit in any universe.

Equations

• ParseIt.Unitᵤ = PUnit

inductive ParseIt.Boolᵤ : Type u

Bool in any universe.

• false : Boolᵤ

  False.

• true : Boolᵤ

  True.

@[instance_reducible]

instance ParseIt.instDecidableEqBoolᵤ : DecidableEq Boolᵤ

Equations

• ParseIt.instDecidableEqBoolᵤ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ParseIt.instInhabitedBoolᵤ : Inhabited Boolᵤ

Equations

• ParseIt.instInhabitedBoolᵤ = { default := ParseIt.instInhabitedBoolᵤ.default }

def ParseIt.Boolᵤ.toBool : Boolᵤ → Bool

Convert to Bool.

Equations

• ↑ParseIt.Boolᵤ.false = false
• ↑ParseIt.Boolᵤ.true = true

def ParseIt.Boolᵤ.ofBool : Bool → Boolᵤ

Convert from Bool.

Equations

• ParseIt.Boolᵤ.ofBool false = ParseIt.Boolᵤ.false
• ParseIt.Boolᵤ.ofBool true = ParseIt.Boolᵤ.true

@[instance_reducible]

instance ParseIt.Boolᵤ.instCoeBool : Coe Boolᵤ Bool

Equations

• ParseIt.Boolᵤ.instCoeBool = { coe := ParseIt.Boolᵤ.toBool }

@[instance_reducible]

instance ParseIt.Boolᵤ.instRepr : Repr Boolᵤ

Equations

• ParseIt.Boolᵤ.instRepr = { reprPrec := fun (b : ParseIt.Boolᵤ) => reprPrec ↑b }

@[instance_reducible]

instance ParseIt.Boolᵤ.instToString : ToString Boolᵤ

Equations

• ParseIt.Boolᵤ.instToString = { toString := fun (b : ParseIt.Boolᵤ) => toString ↑b }

structure ParseIt.Natᵤ : Type u

Nat in any universe.

• val : Nat

  The underlying natural number.

def ParseIt.instDecidableEqNatᵤ.decEq (x✝ x✝¹ : Natᵤ) : Decidable (x✝ = x✝¹)

Equations

• ParseIt.instDecidableEqNatᵤ.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ParseIt.instDecidableEqNatᵤ : DecidableEq Natᵤ

Equations

• ParseIt.instDecidableEqNatᵤ = ParseIt.instDecidableEqNatᵤ.decEq

@[instance_reducible]

instance ParseIt.instInhabitedNatᵤ : Inhabited Natᵤ

Equations

• ParseIt.instInhabitedNatᵤ = { default := ParseIt.instInhabitedNatᵤ.default }

@[instance_reducible]

instance ParseIt.Natᵤ.instCoeNat : Coe Natᵤ Nat

Equations

• ParseIt.Natᵤ.instCoeNat = { coe := ParseIt.Natᵤ.val }

@[instance_reducible]

instance ParseIt.Natᵤ.instOfNat (n : Nat) : OfNat Natᵤ n

Equations

• ParseIt.Natᵤ.instOfNat n = { ofNat := { val := n } }

@[instance_reducible]

instance ParseIt.Natᵤ.instRepr : Repr Natᵤ

Equations

• ParseIt.Natᵤ.instRepr = { reprPrec := fun (n : ParseIt.Natᵤ) => reprPrec ↑n }

@[instance_reducible]

instance ParseIt.Natᵤ.instToString : ToString Natᵤ

Equations

• ParseIt.Natᵤ.instToString = { toString := fun (n : ParseIt.Natᵤ) => toString ↑n }