Init.Prelude

instDecidableAnd = match dp with | isTrue hp => match dq with | isTrue hq => isTrue (_ : p ∧ q) | isFalse hq => isFalse (_ : p ∧ q → False) | isFalse hp => isFalse (_ : p ∧ q → False)

source

@[macroInline]

instance instDecidableOr {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] :

Decidable (p ∨ q)

Equations

instDecidableOr = match dp with | isTrue hp => isTrue (_ : p ∨ q) | isFalse hp => match dq with | isTrue hq => isTrue (_ : p ∨ q) | isFalse hq => isFalse (_ : p ∨ q → False)

source

instance instDecidableNot {p : Prop} [dp : Decidable p] :

Decidable ¬p

Equations

instDecidableNot = match dp with | isTrue hp => isFalse (_ : ¬p → False) | isFalse hp => isTrue hp

source

@[macroInline]

def cond {α : Type u} (c : Bool) (x : α) (y : α) :

α

Equations

cond c x y = match c with | true => x | false => y

source

@[macroInline]

def or (x : Bool) (y : Bool) :

Bool

Equations

(x || y) = match x with | true => true | false => y

source

@[macroInline]

def and (x : Bool) (y : Bool) :

Bool

Equations

(x && y) = match x with | false => false | true => y

source

@[inline]

def not :

Bool → Bool

Equations

(!x) = match x with | true => false | false => true

source

inductive Nat :

Type

zero: Nat
succ: Nat → Nat

source

instance instInhabitedNat :

Inhabited Nat

Equations

instInhabitedNat = { default := Nat.zero }

source

class OfNat (α : Type u) (n : Nat) :

Type u

ofNat : α

Instances

source

@[defaultInstance 100]

instance instOfNatNat (n : Nat) :

OfNat Nat n

Equations

instOfNatNat n = { ofNat := n }

source

class LE (α : Type u) :

Type u

le : α → α → Prop

Instances

source

class LT (α : Type u) :

Type u

lt : α → α → Prop

Instances

source

noncomputable def GE.ge {α : Type u} [inst : LE α] (a : α) (b : α) :

Prop

Equations

(a ≥ b) = (b ≤ a)

source

noncomputable def GT.gt {α : Type u} [inst : LT α] (a : α) (b : α) :

Prop

Equations

(a > b) = (b < a)

source

@[inline]

def max {α : Type u_1} [inst : LT α] [inst : DecidableRel LT.lt] (a : α) (b : α) :

α

Equations

max a b = if b < a then a else b

source

@[inline]

def min {α : Type u_1} [inst : LE α] [inst : DecidableRel LE.le] (a : α) (b : α) :

α

Equations

min a b = if a ≤ b then a else b

source

class Trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) :

Type

trans : {a : α} → {b : β} → {c : γ} → r a b → s b c → t a c

Instances

source

instance instTransEq {α : Sort u_1} {γ : Sort u_2} (r : α → γ → Prop) :

Trans Eq r r

Equations

instTransEq r = { trans := @instTransEq.proof_1 α γ r }

source

instance instTransEq_1 {α : Sort u_1} {β : Sort u_2} (r : α → β → Prop) :

Trans r Eq r

Equations

instTransEq_1 r = { trans := @instTransEq_1.proof_1 α β r }

source

class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hAdd : α → β → γ

Instances

instHAdd

source

class HSub (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hSub : α → β → γ

Instances

instHSub

source

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hMul : α → β → γ

Instances

instHMul

source

class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hDiv : α → β → γ

Instances

source

class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hMod : α → β → γ

Instances

source

class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hPow : α → β → γ

Instances

source

class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hAppend : α → β → γ

Instances

source

class HOrElse (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hOrElse : α → (Unit → β) → γ

Instances

instHOrElse

source

class HAndThen (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hAndThen : α → (Unit → β) → γ

Instances

instHAndThen

source

class HAnd (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hAnd : α → β → γ

Instances

instHAnd

source

class HXor (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hXor : α → β → γ

Instances

instHXor

source

class HOr (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hOr : α → β → γ

Instances

instHOr

source

class HShiftLeft (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hShiftLeft : α → β → γ

Instances

instHShiftLeft

source

class HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) :

Type (max (max u v) w)

hShiftRight : α → β → γ

Instances

instHShiftRight

source

class Add (α : Type u) :

Type u

add : α → α → α

Instances

source

class Sub (α : Type u) :

Type u

sub : α → α → α

Instances

source

class Mul (α : Type u) :

Type u

mul : α → α → α

Instances

source

class Neg (α : Type u) :

Type u

neg : α → α

Instances

source

class Div (α : Type u) :

Type u

div : α → α → α

Instances

source

class Mod (α : Type u) :

Type u

mod : α → α → α

Instances

source

class Pow (α : Type u) (β : Type v) :

Type (max u v)

pow : α → β → α

Instances

source

class Append (α : Type u) :

Type u

append : α → α → α

Instances

source

class OrElse (α : Type u) :

Type u

orElse : α → (Unit → α) → α

Instances

source

class AndThen (α : Type u) :

Type u

andThen : α → (Unit → α) → α

Instances

source

class AndOp (α : Type u) :

Type u

and : α → α → α

Instances

source

class Xor (α : Type u) :

Type u

xor : α → α → α

Instances

source

class OrOp (α : Type u) :

Type u

or : α → α → α

Instances

source

class Complement (α : Type u) :

Type u

complement : α → α

Instances

source

class ShiftLeft (α : Type u) :

Type u

shiftLeft : α → α → α

Instances

source

class ShiftRight (α : Type u) :

Type u

shiftRight : α → α → α

Instances

source

@[defaultInstance 1000]

instance instHAdd {α : Type u_1} [inst : Add α] :

HAdd α α α

Equations

instHAdd = { hAdd := fun a b => Add.add a b }

source

@[defaultInstance 1000]

instance instHSub {α : Type u_1} [inst : Sub α] :

HSub α α α

Equations

instHSub = { hSub := fun a b => Sub.sub a b }

source

@[defaultInstance 1000]

instance instHMul {α : Type u_1} [inst : Mul α] :

HMul α α α

Equations

instHMul = { hMul := fun a b => Mul.mul a b }

source

@[defaultInstance 1000]

instance instHDiv {α : Type u_1} [inst : Div α] :

HDiv α α α

Equations

instHDiv = { hDiv := fun a b => Div.div a b }

source

@[defaultInstance 1000]

instance instHMod {α : Type u_1} [inst : Mod α] :

HMod α α α

Equations

instHMod = { hMod := fun a b => Mod.mod a b }

source

@[defaultInstance 1000]

instance instHPow {α : Type u_1} {β : Type u_2} [inst : Pow α β] :

HPow α β α

Equations

instHPow = { hPow := fun a b => Pow.pow a b }

source

@[defaultInstance 1000]

instance instHAppend {α : Type u_1} [inst : Append α] :

HAppend α α α

Equations

instHAppend = { hAppend := fun a b => Append.append a b }

source

@[defaultInstance 1000]

instance instHOrElse {α : Type u_1} [inst : OrElse α] :

HOrElse α α α

Equations

instHOrElse = { hOrElse := fun a b => OrElse.orElse a b }

source

@[defaultInstance 1000]

instance instHAndThen {α : Type u_1} [inst : AndThen α] :

HAndThen α α α

Equations

instHAndThen = { hAndThen := fun a b => AndThen.andThen a b }

source

@[defaultInstance 1000]

instance instHAnd {α : Type u_1} [inst : AndOp α] :

HAnd α α α

Equations

instHAnd = { hAnd := fun a b => AndOp.and a b }

source

@[defaultInstance 1000]

instance instHXor {α : Type u_1} [inst : Xor α] :

HXor α α α

Equations

instHXor = { hXor := fun a b => Xor.xor a b }

source

@[defaultInstance 1000]

instance instHOr {α : Type u_1} [inst : OrOp α] :

HOr α α α

Equations

instHOr = { hOr := fun a b => OrOp.or a b }

source

@[defaultInstance 1000]

instance instHShiftLeft {α : Type u_1} [inst : ShiftLeft α] :

HShiftLeft α α α

Equations

instHShiftLeft = { hShiftLeft := fun a b => ShiftLeft.shiftLeft a b }

source

@[defaultInstance 1000]

instance instHShiftRight {α : Type u_1} [inst : ShiftRight α] :

HShiftRight α α α

Equations

instHShiftRight = { hShiftRight := fun a b => ShiftRight.shiftRight a b }

source

@[matchPattern, extern lean_nat_add]

def Nat.add :

Nat → Nat → Nat

Equations

Nat.add x Nat.zero = x
Nat.add x (Nat.succ b) = Nat.succ (Nat.add x b)

source

instance instAddNat :

Add Nat

Equations

instAddNat = { add := Nat.add }

source

@[extern lean_nat_mul]

def Nat.mul :

Nat → Nat → Nat

Equations

Nat.mul x 0 = 0
Nat.mul x (Nat.succ b) = Nat.add (Nat.mul x b) x

source

instance instMulNat :

Mul Nat

Equations

instMulNat = { mul := Nat.mul }

source

@[extern lean_nat_pow]

def Nat.pow (m : Nat) :

Nat → Nat

Equations

Nat.pow m 0 = 1
Nat.pow m (Nat.succ n) = Nat.mul (Nat.pow m n) m

source

instance instPowNat :

Pow Nat Nat

Equations

instPowNat = { pow := Nat.pow }

source

@[extern lean_nat_dec_eq]

def Nat.beq :

Nat → Nat → Bool

Equations

Nat.beq Nat.zero Nat.zero = true
Nat.beq Nat.zero (Nat.succ m) = false
Nat.beq (Nat.succ n) Nat.zero = false
Nat.beq (Nat.succ n) (Nat.succ m) = Nat.beq n m

source

theorem Nat.eq_of_beq_eq_true {n : Nat} {m : Nat} :

Nat.beq n m = true → n = m

source

theorem Nat.ne_of_beq_eq_false {n : Nat} {m : Nat} :

Nat.beq n m = false → ¬n = m

source

@[extern lean_nat_dec_eq]

def Nat.decEq (n : Nat) (m : Nat) :

Decidable (n = m)

Equations

Nat.decEq n m = match Nat.beq n m, (_ : Nat.beq n m = Nat.beq n m) with | true, h => isTrue (_ : n = m) | false, h => isFalse (_ : ¬n = m)

source

@[inline]

instance instDecidableEqNat :

DecidableEq Nat

Equations

instDecidableEqNat = Nat.decEq

source

@[extern lean_nat_dec_le]

def Nat.ble :

Nat → Nat → Bool

Equations

Nat.ble Nat.zero Nat.zero = true
Nat.ble Nat.zero (Nat.succ m) = true
Nat.ble (Nat.succ n) Nat.zero = false
Nat.ble (Nat.succ n) (Nat.succ m) = Nat.ble n m

source

inductive Nat.le (n : Nat) :

Nat → Prop

refl: ∀ {n : Nat}, Nat.le n n
step: ∀ {n m : Nat}, Nat.le n m → Nat.le n (Nat.succ m)

source

instance instLENat :

LE Nat

Equations

instLENat = { le := Nat.le }

source

noncomputable def Nat.lt (n : Nat) (m : Nat) :

Prop

Equations

Nat.lt n m = Nat.le (Nat.succ n) m

source

instance instLTNat :

LT Nat

Equations

instLTNat = { lt := Nat.lt }

source

theorem Nat.not_succ_le_zero (n : Nat) :

Nat.succ n ≤ 0 → False

source

theorem Nat.not_lt_zero (n : Nat) :

¬n < 0

source

theorem Nat.zero_le (n : Nat) :

0 ≤ n

source

theorem Nat.succ_le_succ {n : Nat} {m : Nat} :

n ≤ m → Nat.succ n ≤ Nat.succ m

source

theorem Nat.zero_lt_succ (n : Nat) :

0 < Nat.succ n

source

theorem Nat.le_step {n : Nat} {m : Nat} (h : n ≤ m) :

n ≤ Nat.succ m

source

theorem Nat.le_trans {n : Nat} {m : Nat} {k : Nat} :

n ≤ m → m ≤ k → n ≤ k

source

theorem Nat.lt_trans {n : Nat} {m : Nat} {k : Nat} (h₁ : n < m) :

m < k → n < k

source

theorem Nat.le_succ (n : Nat) :

n ≤ Nat.succ n

source

theorem Nat.le_succ_of_le {n : Nat} {m : Nat} (h : n ≤ m) :

n ≤ Nat.succ m

source

theorem Nat.le_refl (n : Nat) :

n ≤ n

source

theorem Nat.succ_pos (n : Nat) :

0 < Nat.succ n

source

@[extern c inline "lean_nat_sub(#1, lean_box(1))"]

def Nat.pred :

Nat → Nat

Equations

Nat.pred x = match x with | 0 => 0 | Nat.succ a => a

source

theorem Nat.pred_le_pred {n : Nat} {m : Nat} :

n ≤ m → Nat.pred n ≤ Nat.pred m

source

theorem Nat.le_of_succ_le_succ {n : Nat} {m : Nat} :

Nat.succ n ≤ Nat.succ m → n ≤ m

source

theorem Nat.le_of_lt_succ {m : Nat} {n : Nat} :

m < Nat.succ n → m ≤ n

source

theorem Nat.eq_or_lt_of_le {n : Nat} {m : Nat} :

n ≤ m → n = m ∨ n < m

source

theorem Nat.lt_or_ge (n : Nat) (m : Nat) :

n < m ∨ n ≥ m

source

theorem Nat.not_succ_le_self (n : Nat) :

¬Nat.succ n ≤ n

source

theorem Nat.lt_irrefl (n : Nat) :

¬n < n

source

theorem Nat.lt_of_le_of_lt {n : Nat} {m : Nat} {k : Nat} (h₁ : n ≤ m) (h₂ : m < k) :

n < k

source

theorem Nat.le_antisymm {n : Nat} {m : Nat} (h₁ : n ≤ m) (h₂ : m ≤ n) :

n = m

source

theorem Nat.lt_of_le_of_ne {n : Nat} {m : Nat} (h₁ : n ≤ m) (h₂ : ¬n = m) :

n < m

source

theorem Nat.le_of_ble_eq_true {n : Nat} {m : Nat} (h : Nat.ble n m = true) :

n ≤ m

source

theorem Nat.ble_self_eq_true (n : Nat) :

Nat.ble n n = true

source

theorem Nat.ble_succ_eq_true {n : Nat} {m : Nat} :

Nat.ble n m = true → Nat.ble n (Nat.succ m) = true

source

theorem Nat.ble_eq_true_of_le {n : Nat} {m : Nat} (h : n ≤ m) :

Nat.ble n m = true

source

theorem Nat.not_le_of_not_ble_eq_true {n : Nat} {m : Nat} (h : ¬Nat.ble n m = true) :

¬n ≤ m

source

@[extern lean_nat_dec_le]

instance Nat.decLe (n : Nat) (m : Nat) :

Decidable (n ≤ m)

Equations

Nat.decLe n m = if h : Nat.ble n m = true then isTrue (_ : n ≤ m) else isFalse (_ : ¬n ≤ m)

source

@[extern lean_nat_dec_lt]

instance Nat.decLt (n : Nat) (m : Nat) :

Decidable (n < m)

Equations

Nat.decLt n m = Nat.decLe (Nat.succ n) m

source

@[extern lean_nat_sub]

def Nat.sub :

Nat → Nat → Nat

Equations

Nat.sub x 0 = x
Nat.sub x (Nat.succ b) = Nat.pred (Nat.sub x b)

source

instance instSubNat :

Sub Nat

Equations

instSubNat = { sub := Nat.sub }

source

@[extern lean_system_platform_nbits]

constant System.Platform.getNumBits :

Unit → { n // n = 32 ∨ n = 64 }

source

def System.Platform.numBits :

Nat

Equations

System.Platform.numBits = (System.Platform.getNumBits ()).val

source

theorem System.Platform.numBits_eq :

System.Platform.numBits = 32 ∨ System.Platform.numBits = 64

source

structure Fin (n : Nat) :

Type

val : Nat
isLt : val < n

source

theorem Fin.eq_of_val_eq {n : Nat} {i : Fin n} {j : Fin n} :

i.val = j.val → i = j

source

theorem Fin.val_eq_of_eq {n : Nat} {i : Fin n} {j : Fin n} (h : i = j) :

i.val = j.val

source

theorem Fin.ne_of_val_ne {n : Nat} {i : Fin n} {j : Fin n} (h : ¬i.val = j.val) :

¬i = j

source

instance instDecidableEqFin (n : Nat) :

DecidableEq (Fin n)

Equations

instDecidableEqFin n i j = match decEq i.val j.val with | isTrue h => isTrue (_ : i = j) | isFalse h => isFalse (_ : ¬i = j)

source

instance instLTFin {n : Nat} :

LT (Fin n)

Equations

instLTFin = { lt := fun a b => a.val < b.val }

source

instance instLEFin {n : Nat} :

LE (Fin n)

Equations

instLEFin = { le := fun a b => a.val ≤ b.val }

source

instance Fin.decLt {n : Nat} (a : Fin n) (b : Fin n) :

Decidable (a < b)

Equations

Fin.decLt a b = Nat.decLt a.val b.val

source

instance Fin.decLe {n : Nat} (a : Fin n) (b : Fin n) :

Decidable (a ≤ b)

Equations

Fin.decLe a b = Nat.decLe a.val b.val

source

def UInt8.size :

Nat

Equations

UInt8.size = 256

source

structure UInt8 :

Type

val : Fin UInt8.size

source

@[extern lean_uint8_of_nat]

def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) :

UInt8

Equations

UInt8.ofNatCore n h = { val := { val := n, isLt := h } }

source

@[extern lean_uint8_dec_eq]

def UInt8.decEq (a : UInt8) (b : UInt8) :

Decidable (a = b)

Equations

UInt8.decEq a b = match a, b with | { val := n }, { val := m } => if h : n = m then isTrue (_ : { val := n } = { val := m }) else isFalse (_ : { val := n } = { val := m } → False)

source

instance instDecidableEqUInt8 :

DecidableEq UInt8

Equations

instDecidableEqUInt8 = UInt8.decEq

source

instance instInhabitedUInt8 :

Inhabited UInt8

Equations

instInhabitedUInt8 = { default := UInt8.ofNatCore 0 instInhabitedUInt8.proof_1 }

source

def UInt16.size :

Nat

Equations

UInt16.size = 65536

source

structure UInt16 :

Type

val : Fin UInt16.size

source

@[extern lean_uint16_of_nat]

def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) :

UInt16

Equations

UInt16.ofNatCore n h = { val := { val := n, isLt := h } }

source

@[extern lean_uint16_dec_eq]

def UInt16.decEq (a : UInt16) (b : UInt16) :

Decidable (a = b)

Equations

UInt16.decEq a b = match a, b with | { val := n }, { val := m } => if h : n = m then isTrue (_ : { val := n } = { val := m }) else isFalse (_ : { val := n } = { val := m } → False)

source

instance instDecidableEqUInt16 :

DecidableEq UInt16

Equations

instDecidableEqUInt16 = UInt16.decEq

source

instance instInhabitedUInt16 :

Inhabited UInt16

Equations

instInhabitedUInt16 = { default := UInt16.ofNatCore 0 instInhabitedUInt16.proof_1 }

source

def UInt32.size :

Nat

Equations

UInt32.size = 4294967296

source

structure UInt32 :

Type

val : Fin UInt32.size

source

@[extern lean_uint32_of_nat]

def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) :

UInt32

Equations

UInt32.ofNatCore n h = { val := { val := n, isLt := h } }

source

@[extern lean_uint32_to_nat]

def UInt32.toNat (n : UInt32) :

Nat

Equations

UInt32.toNat n = n.val.val

source

@[extern lean_uint32_dec_eq]

def UInt32.decEq (a : UInt32) (b : UInt32) :

Decidable (a = b)

Equations

UInt32.decEq a b = match a, b with | { val := n }, { val := m } => if h : n = m then isTrue (_ : { val := n } = { val := m }) else isFalse (_ : { val := n } = { val := m } → False)

source

instance instDecidableEqUInt32 :

DecidableEq UInt32

Equations

instDecidableEqUInt32 = UInt32.decEq

source

instance instInhabitedUInt32 :

Inhabited UInt32

Equations

instInhabitedUInt32 = { default := UInt32.ofNatCore 0 instInhabitedUInt32.proof_1 }

source

instance instLTUInt32 :

LT UInt32

Equations

instLTUInt32 = { lt := fun a b => a.val < b.val }

source

instance instLEUInt32 :

LE UInt32

Equations

instLEUInt32 = { le := fun a b => a.val ≤ b.val }

source

@[extern lean_uint32_dec_lt]

def UInt32.decLt (a : UInt32) (b : UInt32) :

Decidable (a < b)

Equations

UInt32.decLt a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))

source

@[extern lean_uint32_dec_le]

def UInt32.decLe (a : UInt32) (b : UInt32) :

Decidable (a ≤ b)

Equations

UInt32.decLe a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))

source

instance instDecidableLtUInt32InstLTUInt32 (a : UInt32) (b : UInt32) :

Decidable (a < b)

Equations

instDecidableLtUInt32InstLTUInt32 a b = UInt32.decLt a b

source

instance instDecidableLeUInt32InstLEUInt32 (a : UInt32) (b : UInt32) :

Decidable (a ≤ b)

Equations

instDecidableLeUInt32InstLEUInt32 a b = UInt32.decLe a b

source

def UInt64.size :

Nat

Equations

UInt64.size = 18446744073709551616

source

structure UInt64 :

Type

val : Fin UInt64.size

source

@[extern lean_uint64_of_nat]

def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) :

UInt64

Equations

UInt64.ofNatCore n h = { val := { val := n, isLt := h } }

source

@[extern lean_uint64_dec_eq]

def UInt64.decEq (a : UInt64) (b : UInt64) :

Decidable (a = b)

Equations

UInt64.decEq a b = match a, b with | { val := n }, { val := m } => if h : n = m then isTrue (_ : { val := n } = { val := m }) else isFalse (_ : { val := n } = { val := m } → False)

source

instance instDecidableEqUInt64 :

DecidableEq UInt64

Equations

instDecidableEqUInt64 = UInt64.decEq

source

instance instInhabitedUInt64 :

Inhabited UInt64

Equations

instInhabitedUInt64 = { default := UInt64.ofNatCore 0 instInhabitedUInt64.proof_1 }

source

def USize.size :

Nat

Equations

USize.size = 2 ^ System.Platform.numBits

source

theorem usize_size_eq :

USize.size = 4294967296 ∨ USize.size = 18446744073709551616

source

structure USize :

Type

val : Fin USize.size

source

@[extern lean_usize_of_nat]

def USize.ofNatCore (n : Nat) (h : n < USize.size) :

USize

Equations

USize.ofNatCore n h = { val := { val := n, isLt := h } }

source

@[extern lean_usize_dec_eq]

def USize.decEq (a : USize) (b : USize) :

Decidable (a = b)

Equations

USize.decEq a b = match a, b with | { val := n }, { val := m } => if h : n = m then isTrue (_ : { val := n } = { val := m }) else isFalse (_ : { val := n } = { val := m } → False)

source

instance instDecidableEqUSize :

DecidableEq USize

Equations

instDecidableEqUSize = USize.decEq

source

instance instInhabitedUSize :

Inhabited USize

Equations

instInhabitedUSize = { default := USize.ofNatCore 0 instInhabitedUSize.proof_1 }

source

@[extern lean_usize_of_nat]

def USize.ofNat32 (n : Nat) (h : n < 4294967296) :

USize

Equations

USize.ofNat32 n h = { val := { val := n, isLt := (_ : n < USize.size) } }

source

@[inline]

abbrev Nat.isValidChar (n : Nat) :

Prop

Equations

Nat.isValidChar n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

source

@[inline]

abbrev UInt32.isValidChar (n : UInt32) :

Prop

Equations

UInt32.isValidChar n = Nat.isValidChar (UInt32.toNat n)

source

structure Char :

Type

val : UInt32
valid : UInt32.isValidChar val

source

@[extern lean_uint32_of_nat]

def Char.ofNatAux (n : Nat) (h : Nat.isValidChar n) :

Char

Equations

Char.ofNatAux n h = { val := { val := { val := n, isLt := (_ : n < UInt32.size) } }, valid := h }

source

@[matchPattern, noinline]

def Char.ofNat (n : Nat) :

Char

Equations

Char.ofNat n = if h : Nat.isValidChar n then Char.ofNatAux n h else { val := { val := { val := 0, isLt := Char.ofNat.proof_1 } }, valid := Char.ofNat.proof_2 }

source

theorem Char.eq_of_val_eq {c : Char} {d : Char} :

c.val = d.val → c = d

source

theorem Char.val_eq_of_eq {c : Char} {d : Char} :

c = d → c.val = d.val

source

theorem Char.ne_of_val_ne {c : Char} {d : Char} (h : ¬c.val = d.val) :

¬c = d

source

theorem Char.val_ne_of_ne {c : Char} {d : Char} (h : ¬c = d) :

¬c.val = d.val

source

instance instDecidableEqChar :

DecidableEq Char

Equations

instDecidableEqChar c d = match decEq c.val d.val with | isTrue h => isTrue (_ : c = d) | isFalse h => isFalse (_ : ¬c = d)

source

def Char.utf8Size (c : Char) :

UInt32

Equations

Char.utf8Size c = let v := c.val; if v ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2 else if v ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4 else if v ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6 else UInt32.ofNatCore 4 Char.utf8Size.proof_7

source

@[unbox]

inductive Option (α : Type u) :

Type u

none: {α : Type u} → Option α
some: {α : Type u} → α → Option α

source

instance instInhabitedOption {α : Type u_1} :

Inhabited (Option α)

Equations

instInhabitedOption = { default := none }

source

@[macroInline]

def Option.getD {α : Type u_1} :

Option α → α → α

Equations

Option.getD x x = match x, x with | some x, x_1 => x | none, e => e

source

inductive List (α : Type u) :

Type u

nil: {α : Type u} → List α
cons: {α : Type u} → α → List α → List α

source

instance instInhabitedList {α : Type u_1} :

Inhabited (List α)

Equations

instInhabitedList = { default := [] }

source

def List.hasDecEq {α : Type u} [inst : DecidableEq α] (a : List α) (b : List α) :

Decidable (a = b)

Equations

List.hasDecEq [] [] = isTrue (_ : [] = [])
List.hasDecEq (a :: as) [] = isFalse (_ : a :: as = [] → List.noConfusionType False (a :: as) [])
List.hasDecEq [] (b :: bs) = isFalse (_ : [] = b :: bs → List.noConfusionType False [] (b :: bs))
List.hasDecEq (a :: as) (b :: bs) = match decEq a b with | isTrue hab => match List.hasDecEq as bs with | isTrue habs => isTrue (_ : a :: as = b :: bs) | isFalse nabs => isFalse (_ : a :: as = b :: bs → False) | isFalse nab => isFalse (_ : a :: as = b :: bs → False)

source

instance instDecidableEqList {α : Type u} [inst : DecidableEq α] :

DecidableEq (List α)

Equations

instDecidableEqList = List.hasDecEq

source

@[specialize]

def List.foldl {α : Sort u_1} {β : Type u_2} (f : α → β → α) (init : α) :

List β → α

Equations

List.foldl f x [] = x
List.foldl f x (b :: l) = List.foldl f (f x b) l

source

def List.set {α : Type u_1} :

List α → Nat → α → List α

Equations

List.set (a :: as) 0 x = x :: as
List.set (a :: as) (Nat.succ n) x = a :: List.set as n x
List.set [] x x = []

source

def List.length {α : Type u_1} :

List α → Nat

Equations

List.length [] = 0
List.length (a :: as) = List.length as + 1

source

def List.lengthTRAux {α : Type u_1} :

List α → Nat → Nat

Equations

List.lengthTRAux [] x = x
List.lengthTRAux (a :: as) x = List.lengthTRAux as (Nat.succ x)

source

def List.lengthTR {α : Type u_1} (as : List α) :

Nat

Equations

List.lengthTR as = List.lengthTRAux as 0

source

@[simp]

theorem List.length_cons {α : Type u_1} (a : α) (as : List α) :

List.length (a :: as) = Nat.succ (List.length as)

source

def List.concat {α : Type u} :

List α → α → List α

Equations

List.concat [] x = [x]
List.concat (a :: as) x = a :: List.concat as x

source

def List.get {α : Type u} (as : List α) (i : Nat) :

i < List.length as → α

Equations

List.get [] x x = absurd x (_ : ¬x < 0)
List.get (a :: as) 0 h = a
List.get (a :: as) (Nat.succ i) h = (fun this => List.get as i (_ : Nat.succ i ≤ List.length as)) (_ : Nat.succ i < Nat.succ (List.length as))

source

structure String :

Type

data : List Char

source

@[extern lean_string_dec_eq]

def String.decEq (s₁ : String) (s₂ : String) :

Decidable (s₁ = s₂)

Equations

String.decEq s₁ s₂ = match s₁, s₂ with | { data := s₁ }, { data := s₂ } => if h : s₁ = s₂ then isTrue (_ : { data := s₁ } = { data := s₂ }) else isFalse (_ : { data := s₁ } = { data := s₂ } → False)

source

instance instDecidableEqString :

DecidableEq String

Equations

instDecidableEqString = String.decEq

source

@[inline]

abbrev String.Pos :

Type

Equations

String.Pos = Nat

source

structure Substring :

Type

str : String
startPos : String.Pos
stopPos : String.Pos

source

instance instInhabitedSubstring :

Inhabited Substring

Equations

instInhabitedSubstring = { default := { str := "", startPos := 0, stopPos := 0 } }

source

@[inline]

def Substring.bsize :

Substring → Nat

Equations

Substring.bsize x = match x with | { str := x, startPos := b, stopPos := e } => Nat.sub e b

source

def String.csize (c : Char) :

Nat

Equations

String.csize c = UInt32.toNat (Char.utf8Size c)

source

@[extern lean_string_utf8_byte_size]

def String.utf8ByteSize :

String → Nat

Equations

String.utf8ByteSize x = match x with | { data := s } => String.utf8ByteSizeAux s 0

source

@[inline]

def String.bsize (s : String) :

Nat

Equations

String.bsize s = String.utf8ByteSize s

source

@[inline]

def String.toSubstring (s : String) :

Substring

Equations

String.toSubstring s = { str := s, startPos := 0, stopPos := String.bsize s }

source

unsafe def unsafeCast {α : Type u} {β : Type v} (a : α) :

β

Equations

unsafeCast a = (cast (_ : ULift α = ULift β) { down := a }).down

source

@[neverExtract, extern lean_panic_fn]

constant panicCore {α : Type u} [inst : Inhabited α] (msg : String) :

α

source

@[neverExtract, noinline]

def panic {α : Type u} [inst : Inhabited α] (msg : String) :

α

Equations

panic msg = panicCore msg

source

structure Array (α : Type u) :

Type u

data : List α

source

@[extern lean_mk_empty_array_with_capacity]

def Array.mkEmpty {α : Type u} (c : Nat) :

Array α

Equations

Array.mkEmpty c = { data := [] }

source

def Array.empty {α : Type u} :

Array α

Equations

Array.empty = Array.mkEmpty 0

source

@[extern lean_array_get_size]

def Array.size {α : Type u} (a : Array α) :

Nat

Equations

Array.size a = List.length a.data

source

@[extern lean_array_fget]

def Array.get {α : Type u} (a : Array α) (i : Fin (Array.size a)) :

α

Equations

Array.get a i = List.get a.data i.val (_ : i.val < Array.size a)

source

@[inline]

def Array.getD {α : Type u_1} (a : Array α) (i : Nat) (v₀ : α) :

α

Equations

Array.getD a i v₀ = if h : i < Array.size a then Array.get a { val := i, isLt := h } else v₀

source

@[extern lean_array_get]

def Array.get! {α : Type u} [inst : Inhabited α] (a : Array α) (i : Nat) :

α

Equations

Array.get! a i = Array.getD a i default

source

def Array.getOp {α : Type u} [inst : Inhabited α] (self : Array α) (idx : Nat) :

α

Equations

Array.getOp self idx = Array.get! self idx

source

@[extern lean_array_push]

def Array.push {α : Type u} (a : Array α) (v : α) :

Array α

Equations

Array.push a v = { data := List.concat a.data v }

source

@[extern lean_array_fset]

def Array.set {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) :

Array α

Equations

Array.set a i v = { data := List.set a.data i.val v }

source

@[inline]

def Array.setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) :

Array α

Equations

Array.setD a i v = if h : i < Array.size a then Array.set a { val := i, isLt := h } v else a

source

@[extern lean_array_set]

def Array.set! {α : Type u_1} (a : Array α) (i : Nat) (v : α) :

Array α

Equations

Array.set! a i v = Array.setD a i v

source

def Array.appendCore {α : Type u} (as : Array α) (bs : Array α) :

Array α

Equations

Array.appendCore as bs = (fun loop => loop (Array.size bs) 0 as) (Array.appendCore.loop bs)

source

def Array.appendCore.loop {α : Type u} (bs : Array α) (i : Nat) (j : Nat) (as : Array α) :

Array α

Equations

Array.appendCore.loop bs 0 j as = if hlt : j < Array.size bs then as else as
Array.appendCore.loop bs (Nat.succ i') j as = if hlt : j < Array.size bs then Array.appendCore.loop bs i' (j + 1) (Array.push as (Array.get bs { val := j, isLt := hlt })) else as

source

@[inlineIfReduce]

def List.toArrayAux {α : Type u_1} :

List α → Array α → Array α

Equations

List.toArrayAux [] x = x
List.toArrayAux (a :: as) x = List.toArrayAux as (Array.push x a)

source

@[inlineIfReduce]

def List.redLength {α : Type u_1} :

List α → Nat

Equations

List.redLength [] = 0
List.redLength (a :: as) = Nat.succ (List.redLength as)

source

@[matchPattern, inline]

def List.toArray {α : Type u_1} (as : List α) :

Array α

Equations

List.toArray as = List.toArrayAux as (Array.mkEmpty (List.redLength as))

source

class Bind (m : Type u → Type v) :

Type (max (u + 1) v)

bind : {α β : Type u} → m α → (α → m β) → m β

Instances

Monad.toBind

source

class Pure (f : Type u → Type v) :

Type (max (u + 1) v)

pure : {α : Type u} → α → f α

Instances

Applicative.toPure

source

class Functor (f : Type u → Type v) :

Type (max (u + 1) v)

map : {α β : Type u} → (α → β) → f α → f β
mapConst : {α β : Type u} → α → f β → f α

Instances

source

class Seq (f : Type u → Type v) :

Type (max (u + 1) v)

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

Instances

Applicative.toSeq

source

class SeqLeft (f : Type u → Type v) :

Type (max (u + 1) v)

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

Instances

Applicative.toSeqLeft

source

class SeqRight (f : Type u → Type v) :

Type (max (u + 1) v)

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

Instances

Applicative.toSeqRight

source

class Applicative (f : Type u → Type v) extends Functor , Pure , Seq , SeqLeft , SeqRight :

Type (max (u + 1) v)

Instances

source

instance instInhabitedForAll_2 {α : Type u} {m : Type u → Type v} [inst : Monad m] :

Inhabited (α → m α)

Equations

instInhabitedForAll_2 = { default := pure }

source

instance instInhabited {α : Type u} {m : Type u → Type v} [inst : Monad m] [inst : Inhabited α] :

Inhabited (m α)

Equations

instInhabited = { default := pure default }

source

def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : α → m β) :

m (Array β)

Equations

Array.sequenceMap as f = (fun loop => loop (Array.size as) 0 Array.empty) (Array.sequenceMap.loop as f)

source

def Array.sequenceMap.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : α → m β) (i : Nat) (j : Nat) (bs : Array β) :

m (Array β)

Equations

Array.sequenceMap.loop as f 0 j bs = if hlt : j < Array.size as then pure bs else pure bs
Array.sequenceMap.loop as f (Nat.succ i') j bs = if hlt : j < Array.size as then do let b ← f (Array.get as { val := j, isLt := hlt }) Array.sequenceMap.loop as f i' (j + 1) (Array.push bs b) else pure bs

source

class MonadLift (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

monadLift : {α : Type u} → m α → n α

Instances

source

class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

monadLift : {α : Type u} → m α → n α

Instances

source

@[inline]

abbrev liftM {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1} :

m α → n α

Equations

@liftM = @monadLift

source

instance instMonadLiftT (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [inst : MonadLift n o] [inst : MonadLiftT m n] :

MonadLiftT m o

Equations

instMonadLiftT m n o = { monadLift := fun {α} x => MonadLift.monadLift (monadLift x) }

source

instance instMonadLiftT_1 (m : Type u_1 → Type u_2) :

MonadLiftT m m

Equations

instMonadLiftT_1 m = { monadLift := fun {α} x => x }

source

class MonadFunctor (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Instances

source

class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) :

Type (max (max (u + 1) v) w)

monadMap : {α : Type u} → ({β : Type u} → m β → m β) → n α → n α

Instances

source

instance instMonadFunctorT (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [inst : MonadFunctor n o] [inst : MonadFunctorT m n] :

MonadFunctorT m o

Equations

instMonadFunctorT m n o = { monadMap := fun {α} f => MonadFunctor.monadMap fun {β} => monadMap fun {β} => f β }

source

instance monadFunctorRefl (m : Type u_1 → Type u_2) :

MonadFunctorT m m

Equations

monadFunctorRefl m = { monadMap := fun {α} f => f α }

source

@[unbox]

inductive Except (ε : Type u) (α : Type v) :

Type (max u v)

error: {ε : Type u} → {α : Type v} → ε → Except ε α
ok: {ε : Type u} → {α : Type v} → α → Except ε α

source

instance instInhabitedExcept {ε : Type u} {α : Type v} [inst : Inhabited ε] :

Inhabited (Except ε α)

Equations

instInhabitedExcept = { default := Except.error default }

source

class MonadExceptOf (ε : Type u) (m : Type v → Type w) :

Type (max (max u (v + 1)) w)

throw : {α : Type v} → ε → m α
tryCatch : {α : Type v} → m α → (ε → m α) → m α

Instances

source

@[inline]

abbrev throwThe (ε : Type u) {m : Type v → Type w} [inst : MonadExceptOf ε m] {α : Type v} (e : ε) :

m α

Equations

throwThe ε e = MonadExceptOf.throw e

source

@[inline]

abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [inst : MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) :

m α

Equations

tryCatchThe ε x handle = MonadExceptOf.tryCatch x handle

source

class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :

Type (max (max u (v + 1)) w)

throw : {α : Type v} → ε → m α
tryCatch : {α : Type v} → m α → (ε → m α) → m α

Instances

source

instance instMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [inst : MonadExceptOf ε m] :

MonadExcept ε m

Equations

instMonadExcept ε m = { throw := fun {α} => throwThe ε, tryCatch := fun {α} => tryCatchThe ε }

source

@[inline]

def MonadExcept.orElse {ε : Type u} {m : Type v → Type w} [inst : MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) :

m α

Equations

MonadExcept.orElse t₁ t₂ = tryCatch t₁ fun x => t₂ ()

source

instance MonadExcept.instOrElse {ε : Type u} {m : Type v → Type w} [inst : MonadExcept ε m] {α : Type v} :

OrElse (m α)

Equations

MonadExcept.instOrElse = { orElse := MonadExcept.orElse }

source

noncomputable def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) :

Type (max u v)

Equations

ReaderT ρ m α = (ρ → m α)

source

instance instInhabitedReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) [inst : Inhabited (m α)] :

Inhabited (ReaderT ρ m α)

Equations

instInhabitedReaderT ρ m α = { default := fun x => default }

source

@[inline]

def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) :

m α

Equations

ReaderT.run x r = x r

source

instance ReaderT.instMonadLiftReaderT {ρ : Type u} {m : Type u → Type v} :

MonadLift m (ReaderT ρ m)

Equations

ReaderT.instMonadLiftReaderT = { monadLift := fun {α} x x_1 => x }

source

instance ReaderT.instMonadExceptOfReaderT {ρ : Type u} {m : Type u → Type v} (ε : Type u_1) [inst : MonadExceptOf ε m] :

MonadExceptOf ε (ReaderT ρ m)

Equations

ReaderT.instMonadExceptOfReaderT ε = { throw := fun {α} e => liftM (throw e), tryCatch := fun {α} x c r => tryCatchThe ε (x r) fun e => c e r }

source

@[inline]

def ReaderT.read {ρ : Type u} {m : Type u → Type v} [inst : Monad m] :

ReaderT ρ m ρ

Equations

ReaderT.read = pure

source

@[inline]

def ReaderT.pure {ρ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) :

ReaderT ρ m α

Equations

ReaderT.pure a r = pure a

source

@[inline]

def ReaderT.bind {ρ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) :

ReaderT ρ m β

Equations

ReaderT.bind x f r = do let a ← x r f a r

source

@[inline]

def ReaderT.map {ρ : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → β) (x : ReaderT ρ m α) :

ReaderT ρ m β

Equations

ReaderT.map f x r = f <$> x r

source

instance ReaderT.instMonadReaderT {ρ : Type u} {m : Type u → Type v} [inst : Monad m] :

Monad (ReaderT ρ m)

Equations

ReaderT.instMonadReaderT = Monad.mk

source

instance ReaderT.instMonadFunctorReaderT (ρ : Type u_1) (m : Type u_1 → Type u_2) [inst : Monad m] :

MonadFunctor m (ReaderT ρ m)

Equations

ReaderT.instMonadFunctorReaderT ρ m = { monadMap := fun {α} f x ctx => f α (x ctx) }

source

@[inline]

def ReaderT.adapt {ρ : Type u} {m : Type u → Type v} {ρ' : Type u} [inst : Monad m] {α : Type u} (f : ρ' → ρ) :

ReaderT ρ m α → ReaderT ρ' m α

Equations

ReaderT.adapt f x r = x (f r)

source

class MonadReaderOf (ρ : Type u) (m : Type u → Type v) :

Type v

read : m ρ

Instances

source

@[inline]

def readThe (ρ : Type u) {m : Type u → Type v} [inst : MonadReaderOf ρ m] :

m ρ

Equations

readThe ρ = MonadReaderOf.read

source

class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :

Type v

read : m ρ

Instances

instMonadReader

source

instance instMonadReader (ρ : Type u) (m : Type u → Type v) [inst : MonadReaderOf ρ m] :

MonadReader ρ m

Equations

instMonadReader ρ m = { read := readThe ρ }

source

instance instMonadReaderOf {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [inst : MonadLift m n] [inst : MonadReaderOf ρ m] :

MonadReaderOf ρ n

Equations

instMonadReaderOf = { read := liftM read }

source

instance instMonadReaderOfReaderT {ρ : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadReaderOf ρ (ReaderT ρ m)

Equations

instMonadReaderOfReaderT = { read := ReaderT.read }

source

class MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) :

Type (max (u + 1) v)

withReader : {α : Type u} → (ρ → ρ) → m α → m α

Instances

source

@[inline]

def withTheReader (ρ : Type u) {m : Type u → Type v} [inst : MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) :

m α

Equations

withTheReader ρ f x = MonadWithReaderOf.withReader f x

source

class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) :

Type (max (u + 1) v)

withReader : {α : Type u} → (ρ → ρ) → m α → m α

Instances

instMonadWithReader

source

instance instMonadWithReader (ρ : Type u) (m : Type u → Type v) [inst : MonadWithReaderOf ρ m] :

MonadWithReader ρ m

Equations

instMonadWithReader ρ m = { withReader := fun {α} => withTheReader ρ }

source

instance instMonadWithReaderOf {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [inst : MonadFunctor m n] [inst : MonadWithReaderOf ρ m] :

MonadWithReaderOf ρ n

Equations

instMonadWithReaderOf = { withReader := fun {α} f => monadMap fun {β} => withTheReader ρ f }

source

instance instMonadWithReaderOfReaderT {ρ : Type u} {m : Type u → Type v} [inst : Monad m] :

MonadWithReaderOf ρ (ReaderT ρ m)

Equations

instMonadWithReaderOfReaderT = { withReader := fun {α} f x ctx => x (f ctx) }

source

class MonadStateOf (σ : Type u) (m : Type u → Type v) :

Type (max (u + 1) v)

get : m σ
set : σ → m PUnit
modifyGet : {α : Type u} → (σ → α × σ) → m α

Instances

source

@[inline]

abbrev getThe (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m] :

m σ

Equations

getThe σ = MonadStateOf.get

source

@[inline]

abbrev modifyThe (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m] (f : σ → σ) :

m PUnit

Equations

modifyThe σ f = MonadStateOf.modifyGet fun s => (PUnit.unit, f s)

source

@[inline]

abbrev modifyGetThe {α : Type u} (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m] (f : σ → α × σ) :

m α

Equations

modifyGetThe σ f = MonadStateOf.modifyGet f

source

class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :

Type (max (u + 1) v)

get : m σ
set : σ → m PUnit
modifyGet : {α : Type u} → (σ → α × σ) → m α

Instances

instMonadState

source

instance instMonadState (σ : Type u) (m : Type u → Type v) [inst : MonadStateOf σ m] :

MonadState σ m

Equations

instMonadState σ m = { get := getThe σ, set := set, modifyGet := fun {α} f => MonadStateOf.modifyGet f }

source

@[inline]

def modify {σ : Type u} {m : Type u → Type v} [inst : MonadState σ m] (f : σ → σ) :

m PUnit

Equations

modify f = modifyGet fun s => (PUnit.unit, f s)

source

@[inline]

def getModify {σ : Type u} {m : Type u → Type v} [inst : MonadState σ m] [inst : Monad m] (f : σ → σ) :

m σ

Equations

getModify f = modifyGet fun s => (s, f s)

source

instance instMonadStateOf {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [inst : MonadLift m n] [inst : MonadStateOf σ m] :

MonadStateOf σ n

Equations

instMonadStateOf = { get := liftM MonadStateOf.get, set := fun s => liftM (set s), modifyGet := fun {α} f => monadLift (modifyGet f) }

source

inductive EStateM.Result (ε : Type u) (σ : Type u) (α : Type u) :

Type u

ok: {ε σ α : Type u} → α → σ → EStateM.Result ε σ α
error: {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α

source

instance EStateM.instInhabitedResult {ε : Type u} {σ : Type u} {α : Type u} [inst : Inhabited ε] [inst : Inhabited σ] :

Inhabited (EStateM.Result ε σ α)

Equations

EStateM.instInhabitedResult = { default := EStateM.Result.error default default }

source

noncomputable def EStateM (ε : Type u) (σ : Type u) (α : Type u) :

Type u

Equations

EStateM ε σ α = (σ → EStateM.Result ε σ α)

source

instance EStateM.instInhabitedEStateM {ε : Type u} {σ : Type u} {α : Type u} [inst : Inhabited ε] :

Inhabited (EStateM ε σ α)

Equations

EStateM.instInhabitedEStateM = { default := fun s => EStateM.Result.error default s }

source

@[inline]

def EStateM.pure {ε : Type u} {σ : Type u} {α : Type u} (a : α) :

EStateM ε σ α

Equations

EStateM.pure a s = EStateM.Result.ok a s

source

@[inline]

def EStateM.set {ε : Type u} {σ : Type u} (s : σ) :

EStateM ε σ PUnit

Equations

EStateM.set s x = EStateM.Result.ok PUnit.unit s

source

@[inline]

def EStateM.get {ε : Type u} {σ : Type u} :

EStateM ε σ σ

Equations

EStateM.get s = EStateM.Result.ok s s

source

@[inline]

def EStateM.modifyGet {ε : Type u} {σ : Type u} {α : Type u} (f : σ → α × σ) :

EStateM ε σ α

Equations

EStateM.modifyGet f s = match f s with | (a, s) => EStateM.Result.ok a s

source

@[inline]

def EStateM.throw {ε : Type u} {σ : Type u} {α : Type u} (e : ε) :

EStateM ε σ α

Equations

EStateM.throw e s = EStateM.Result.error e s

source

class EStateM.Backtrackable (δ : outParam (Type u)) (σ : Type u) :

Type u

save : σ → δ
restore : σ → δ → σ

Instances

EStateM.nonBacktrackable

source

@[inline]

def EStateM.tryCatch {ε : Type u} {σ : Type u} {δ : outParam (Type u)} [inst : EStateM.Backtrackable δ σ] {α : Type u} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) :

EStateM ε σ α

Equations

EStateM.tryCatch x handle s = let d := EStateM.Backtrackable.save s; match x s with | EStateM.Result.error e s => handle e (EStateM.Backtrackable.restore s d) | ok => ok

source

@[inline]

def EStateM.orElse {ε : Type u} {σ : Type u} {α : Type u} {δ : outParam (Type u)} [inst : EStateM.Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) :

EStateM ε σ α

Equations

EStateM.orElse x₁ x₂ s = let d := EStateM.Backtrackable.save s; match x₁ s with | EStateM.Result.error x s => x₂ () (EStateM.Backtrackable.restore s d) | ok => ok

source

@[inline]

def EStateM.adaptExcept {ε : Type u} {σ : Type u} {α : Type u} {ε' : Type u} (f : ε → ε') (x : EStateM ε σ α) :

EStateM ε' σ α

Equations

EStateM.adaptExcept f x s = match x s with | EStateM.Result.error e s => EStateM.Result.error (f e) s | EStateM.Result.ok a s => EStateM.Result.ok a s

source

@[inline]

def EStateM.bind {ε : Type u} {σ : Type u} {α : Type u} {β : Type u} (x : EStateM ε σ α) (f : α → EStateM ε σ β) :

EStateM ε σ β

Equations

EStateM.bind x f s = match x s with | EStateM.Result.ok a s => f a s | EStateM.Result.error e s => EStateM.Result.error e s

source

@[inline]

def EStateM.map {ε : Type u} {σ : Type u} {α : Type u} {β : Type u} (f : α → β) (x : EStateM ε σ α) :

EStateM ε σ β

Equations

EStateM.map f x s = match x s with | EStateM.Result.ok a s => EStateM.Result.ok (f a) s | EStateM.Result.error e s => EStateM.Result.error e s

source

@[inline]

def EStateM.seqRight {ε : Type u} {σ : Type u} {α : Type u} {β : Type u} (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) :

EStateM ε σ β

Equations

EStateM.seqRight x y s = match x s with | EStateM.Result.ok x s => y () s | EStateM.Result.error e s => EStateM.Result.error e s

source

instance EStateM.instMonadEStateM {ε : Type u} {σ : Type u} :

Monad (EStateM ε σ)

Equations

EStateM.instMonadEStateM = Monad.mk

source

instance EStateM.instOrElseEStateM {ε : Type u} {σ : Type u} {α : Type u} {δ : outParam (Type u)} [inst : EStateM.Backtrackable δ σ] :

OrElse (EStateM ε σ α)

Equations

EStateM.instOrElseEStateM = { orElse := EStateM.orElse }

source

instance EStateM.instMonadStateOfEStateM {ε : Type u} {σ : Type u} :

MonadStateOf σ (EStateM ε σ)

Equations

EStateM.instMonadStateOfEStateM = { get := EStateM.get, set := EStateM.set, modifyGet := fun {α} => EStateM.modifyGet }

source

instance EStateM.instMonadExceptOfEStateM {ε : Type u} {σ : Type u} {δ : outParam (Type u)} [inst : EStateM.Backtrackable δ σ] :

MonadExceptOf ε (EStateM ε σ)

Equations

EStateM.instMonadExceptOfEStateM = { throw := fun {α} => EStateM.throw, tryCatch := fun {α} => EStateM.tryCatch }

source

@[inline]

def EStateM.run {ε : Type u} {σ : Type u} {α : Type u} (x : EStateM ε σ α) (s : σ) :

EStateM.Result ε σ α

Equations

EStateM.run x s = x s

source

@[inline]

def EStateM.run' {ε : Type u} {σ : Type u} {α : Type u} (x : EStateM ε σ α) (s : σ) :

Option α

Equations

EStateM.run' x s = match EStateM.run x s with | EStateM.Result.ok v x => some v | EStateM.Result.error x x_1 => none

source

@[inline]

def EStateM.dummySave {σ : Type u} :

σ → PUnit

Equations

EStateM.dummySave x = PUnit.unit

source

@[inline]

def EStateM.dummyRestore {σ : Type u} :

σ → PUnit → σ

Equations

EStateM.dummyRestore s x = s

source

instance EStateM.nonBacktrackable {σ : Type u} :

EStateM.Backtrackable PUnit σ

Equations

EStateM.nonBacktrackable = { save := EStateM.dummySave, restore := EStateM.dummyRestore }

source

class Hashable (α : Sort u) :

Sort (max 1 u)

hash : α → UInt64

Instances

source

@[extern lean_uint64_to_usize]

constant UInt64.toUSize (u : UInt64) :

USize

source

@[extern lean_usize_to_uint64]

constant USize.toUInt64 (u : USize) :

UInt64

source

@[extern lean_uint64_mix_hash]

constant mixHash (u₁ : UInt64) (u₂ : UInt64) :

UInt64

source

@[extern lean_string_hash]

constant String.hash (s : String) :

UInt64

source

instance instHashableString :

Hashable String

Equations

instHashableString = { hash := String.hash }

source

inductive Lean.Name :

Type

anonymous: Lean.Name
str: Lean.Name → String → UInt64 → Lean.Name
num: Lean.Name → Nat → UInt64 → Lean.Name

source

instance Lean.instInhabitedName :

Inhabited Lean.Name

Equations

Lean.instInhabitedName = { default := Lean.Name.anonymous }

source

def Lean.Name.hash :

Lean.Name → UInt64

Equations

Lean.Name.hash x = match x with | Lean.Name.anonymous => UInt64.ofNatCore 1723 Lean.Name.hash.proof_1 | Lean.Name.str p s h => h | Lean.Name.num p v h => h

source

instance Lean.instHashableName :

Hashable Lean.Name

Equations

Lean.instHashableName = { hash := Lean.Name.hash }

source

def Lean.Name.mkStr (p : Lean.Name) (s : String) :

Lean.Name

Equations

Lean.Name.mkStr p s = Lean.Name.str p s (mixHash (hash p) (hash s))

source

def Lean.Name.mkNum (p : Lean.Name) (v : Nat) :

Lean.Name

Equations

Lean.Name.mkNum p v = Lean.Name.num p v (mixHash (hash p) (if h : v < UInt64.size then UInt64.ofNatCore v h else UInt64.ofNatCore 17 Lean.Name.mkNum.proof_1))

source

def Lean.Name.mkSimple (s : String) :

Lean.Name

Equations

Lean.Name.mkSimple s = Lean.Name.mkStr Lean.Name.anonymous s

source

@[extern lean_name_eq]

def Lean.Name.beq :

Lean.Name → Lean.Name → Bool

Equations

Lean.Name.beq Lean.Name.anonymous Lean.Name.anonymous = true
Lean.Name.beq (Lean.Name.str p₁ s₁ x_2) (Lean.Name.str p₂ s₂ x_3) = (s₁ == s₂ && Lean.Name.beq p₁ p₂)
Lean.Name.beq (Lean.Name.num p₁ n₁ x_2) (Lean.Name.num p₂ n₂ x_3) = (n₁ == n₂ && Lean.Name.beq p₁ p₂)
Lean.Name.beq x x = false

source

instance Lean.Name.instBEqName :

BEq Lean.Name

Equations

Lean.Name.instBEqName = { beq := Lean.Name.beq }

source

def Lean.Name.append :

Lean.Name → Lean.Name → Lean.Name

Equations

Lean.Name.append x Lean.Name.anonymous = x
Lean.Name.append x (Lean.Name.str p s x_2) = Lean.Name.mkStr (Lean.Name.append x p) s
Lean.Name.append x (Lean.Name.num p d x_2) = Lean.Name.mkNum (Lean.Name.append x p) d

source

instance Lean.Name.instAppendName :

Append Lean.Name

Equations

Lean.Name.instAppendName = { append := Lean.Name.append }

source

inductive Lean.SourceInfo :

Type

original: Substring → String.Pos → Substring → String.Pos → Lean.SourceInfo
synthetic: String.Pos → String.Pos → Lean.SourceInfo
none: Lean.SourceInfo

source

instance Lean.instInhabitedSourceInfo :

Inhabited Lean.SourceInfo

Equations

Lean.instInhabitedSourceInfo = { default := Lean.SourceInfo.none }

source

def Lean.SourceInfo.getPos? (info : Lean.SourceInfo) (originalOnly : optParam Bool false) :

Option String.Pos

Equations

Lean.SourceInfo.getPos? info originalOnly = match info, originalOnly with | Lean.SourceInfo.original x pos x_1 x_2, x_3 => some pos | Lean.SourceInfo.synthetic pos x, false => some pos | x, x_1 => none

source

@[inline]

abbrev Lean.SyntaxNodeKind :

Type

Equations

Lean.SyntaxNodeKind = Lean.Name

source

inductive Lean.Syntax :

Type

missing: Lean.Syntax
node: Lean.SourceInfo → Lean.SyntaxNodeKind → Array Lean.Syntax → Lean.Syntax
atom: Lean.SourceInfo → String → Lean.Syntax
ident: Lean.SourceInfo → Substring → Lean.Name → List (Lean.Name × List String) → Lean.Syntax

source

instance Lean.instInhabitedSyntax :

Inhabited Lean.Syntax

Equations

Lean.instInhabitedSyntax = { default := Lean.Syntax.missing }

source

def Lean.choiceKind :

Lean.SyntaxNodeKind

Equations

Lean.choiceKind = `choice

source

def Lean.nullKind :

Lean.SyntaxNodeKind

Equations

Lean.nullKind = `null

source

def Lean.groupKind :

Lean.SyntaxNodeKind

Equations

Lean.groupKind = `group

source

def Lean.identKind :

Lean.SyntaxNodeKind

Equations

Lean.identKind = `ident

source

def Lean.strLitKind :

Lean.SyntaxNodeKind

Equations

Lean.strLitKind = `strLit

source

def Lean.charLitKind :

Lean.SyntaxNodeKind

Equations

Lean.charLitKind = `charLit

source

def Lean.numLitKind :

Lean.SyntaxNodeKind

Equations

Lean.numLitKind = `numLit

source

def Lean.scientificLitKind :

Lean.SyntaxNodeKind

Equations

Lean.scientificLitKind = `scientificLit

source

def Lean.nameLitKind :

Lean.SyntaxNodeKind

Equations

Lean.nameLitKind = `nameLit

source

def Lean.fieldIdxKind :

Lean.SyntaxNodeKind

Equations

Lean.fieldIdxKind = `fieldIdx

source

def Lean.interpolatedStrLitKind :

Lean.SyntaxNodeKind

Equations

Lean.interpolatedStrLitKind = `interpolatedStrLitKind

source

def Lean.interpolatedStrKind :

Lean.SyntaxNodeKind

Equations

Lean.interpolatedStrKind = `interpolatedStrKind

source

def Lean.Syntax.getKind (stx : Lean.Syntax) :

Lean.SyntaxNodeKind

Equations

Lean.Syntax.getKind stx = match stx with | Lean.Syntax.node x k args => k | Lean.Syntax.missing => `missing | Lean.Syntax.atom x v => Lean.Name.mkSimple v | Lean.Syntax.ident x x_1 x_2 x_3 => Lean.identKind

source

def Lean.Syntax.setKind (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) :

Lean.Syntax

Equations

Lean.Syntax.setKind stx k = match stx with | Lean.Syntax.node info x args => Lean.Syntax.node info k args | x => stx

source

def Lean.Syntax.isOfKind (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) :

Bool

Equations

Lean.Syntax.isOfKind stx k = (Lean.Syntax.getKind stx == k)

source

def Lean.Syntax.getArg (stx : Lean.Syntax) (i : Nat) :

Lean.Syntax

Equations

Lean.Syntax.getArg stx i = match stx with | Lean.Syntax.node x x_1 args => Array.getD args i Lean.Syntax.missing | x => Lean.Syntax.missing

source

@[inline]

def Lean.Syntax.getOp (self : Lean.Syntax) (idx : Nat) :

Lean.Syntax

Equations

Lean.Syntax.getOp self idx = Lean.Syntax.getArg self idx

source

def Lean.Syntax.getArgs (stx : Lean.Syntax) :

Array Lean.Syntax

Equations

Lean.Syntax.getArgs stx = match stx with | Lean.Syntax.node x x_1 args => args | x => Array.empty

source

def Lean.Syntax.getNumArgs (stx : Lean.Syntax) :

Nat

Equations

Lean.Syntax.getNumArgs stx = match stx with | Lean.Syntax.node x x_1 args => Array.size args | x => 0

source

def Lean.Syntax.isMissing :

Lean.Syntax → Bool

Equations

Lean.Syntax.isMissing x = match x with | Lean.Syntax.missing => true | x => false

source

def Lean.Syntax.isNodeOf (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) (n : Nat) :

Bool

Equations

Lean.Syntax.isNodeOf stx k n = (Lean.Syntax.isOfKind stx k && Lean.Syntax.getNumArgs stx == n)

source

def Lean.Syntax.isIdent :

Lean.Syntax → Bool

Equations

Lean.Syntax.isIdent x = match x with | Lean.Syntax.ident x x_1 x_2 x_3 => true | x => false

source

def Lean.Syntax.getId :

Lean.Syntax → Lean.Name

Equations

Lean.Syntax.getId x = match x with | Lean.Syntax.ident x x_1 val x_2 => val | x => Lean.Name.anonymous

source

def Lean.Syntax.matchesNull (stx : Lean.Syntax) (n : Nat) :

Bool

Equations

Lean.Syntax.matchesNull stx n = Lean.Syntax.isNodeOf stx Lean.nullKind n

source

def Lean.Syntax.matchesIdent (stx : Lean.Syntax) (id : Lean.Name) :

Bool

Equations

Lean.Syntax.matchesIdent stx id = (Lean.Syntax.isIdent stx && Lean.Syntax.getId stx == id)

source

def Lean.Syntax.matchesLit (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) (val : String) :

Bool

Equations

Lean.Syntax.matchesLit stx k val = match stx with | Lean.Syntax.node x k' args => k == k' && match Array.getD args 0 Lean.Syntax.missing with | Lean.Syntax.atom x val' => val == val' | x => false | x => false

source

def Lean.Syntax.setArgs (stx : Lean.Syntax) (args : Array Lean.Syntax) :

Lean.Syntax

Equations

Lean.Syntax.setArgs stx args = match stx with | Lean.Syntax.node info k x => Lean.Syntax.node info k args | stx => stx

source

def Lean.Syntax.setArg (stx : Lean.Syntax) (i : Nat) (arg : Lean.Syntax) :

Lean.Syntax

Equations

Lean.Syntax.setArg stx i arg = match stx with | Lean.Syntax.node info k args => Lean.Syntax.node info k (Array.setD args i arg) | stx => stx

source

partial def Lean.Syntax.getHeadInfo? :

Lean.Syntax → Option Lean.SourceInfo

source

partial def Lean.Syntax.getHeadInfo?.loop (args : Array Lean.Syntax) (i : Nat) :

Option Lean.SourceInfo

source

def Lean.Syntax.getHeadInfo (stx : Lean.Syntax) :

Lean.SourceInfo

Equations

Lean.Syntax.getHeadInfo stx = match Lean.Syntax.getHeadInfo? stx with | some info => info | none => Lean.SourceInfo.none

source

def Lean.Syntax.getPos? (stx : Lean.Syntax) (originalOnly : optParam Bool false) :

Option String.Pos

Equations

Lean.Syntax.getPos? stx originalOnly = Lean.SourceInfo.getPos? (Lean.Syntax.getHeadInfo stx) originalOnly

source

partial def Lean.Syntax.getTailPos? (stx : Lean.Syntax) (originalOnly : optParam Bool false) :

Option String.Pos

source

partial def Lean.Syntax.getTailPos?.loop (originalOnly : optParam Bool false) (args : Array Lean.Syntax) (i : Nat) :

Option String.Pos

source

structure Lean.Syntax.SepArray (sep : String) :

Type

elemsAndSeps : Array Lean.Syntax

source

def Lean.SourceInfo.fromRef (ref : Lean.Syntax) :

Lean.SourceInfo

Equations

Lean.SourceInfo.fromRef ref = let _discr := Lean.Syntax.getTailPos? ref; match Lean.Syntax.getPos? ref, Lean.Syntax.getTailPos? ref with | some pos, some tailPos => Lean.SourceInfo.synthetic pos tailPos | x, x_1 => Lean.SourceInfo.none

source

def Lean.mkAtom (val : String) :

Lean.Syntax

Equations

Lean.mkAtom val = Lean.Syntax.atom Lean.SourceInfo.none val

source

def Lean.mkAtomFrom (src : Lean.Syntax) (val : String) :

Lean.Syntax

Equations

Lean.mkAtomFrom src val = Lean.Syntax.atom (Lean.SourceInfo.fromRef src) val

source

inductive Lean.ParserDescr :

Type

const: Lean.Name → Lean.ParserDescr
unary: Lean.Name → Lean.ParserDescr → Lean.ParserDescr
binary: Lean.Name → Lean.ParserDescr → Lean.ParserDescr → Lean.ParserDescr
node: Lean.SyntaxNodeKind → Nat → Lean.ParserDescr → Lean.ParserDescr
trailingNode: Lean.SyntaxNodeKind → Nat → Nat → Lean.ParserDescr → Lean.ParserDescr
symbol: String → Lean.ParserDescr
nonReservedSymbol: String → Bool → Lean.ParserDescr
cat: Lean.Name → Nat → Lean.ParserDescr
parser: Lean.Name → Lean.ParserDescr
nodeWithAntiquot: String → Lean.SyntaxNodeKind → Lean.ParserDescr → Lean.ParserDescr
sepBy: Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr
sepBy1: Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr

source

instance Lean.instInhabitedParserDescr :

Inhabited Lean.ParserDescr

Equations

Lean.instInhabitedParserDescr = { default := Lean.ParserDescr.symbol "" }

source

@[inline]

abbrev Lean.TrailingParserDescr :

Type

Equations

Lean.TrailingParserDescr = Lean.ParserDescr

source

@[inline]

abbrev Lean.MacroScope :

Type

Equations

Lean.MacroScope = Nat

source

def Lean.reservedMacroScope :

Nat

Equations

Lean.reservedMacroScope = 0

source

def Lean.firstFrontendMacroScope :

Nat

Equations

Lean.firstFrontendMacroScope = Lean.reservedMacroScope + 1

source

class Lean.MonadRef (m : Type → Type) :

Type 1

getRef : m Lean.Syntax
withRef : {α : Type} → Lean.Syntax → m α → m α

Instances

source

instance Lean.instMonadRef (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : MonadFunctor m n] [inst : Lean.MonadRef m] :

Lean.MonadRef n

Equations

Lean.instMonadRef m n = { getRef := liftM Lean.getRef, withRef := fun {α} ref x => monadMap (fun {β} => Lean.MonadRef.withRef ref) x }

source

def Lean.replaceRef (ref : Lean.Syntax) (oldRef : Lean.Syntax) :

Lean.Syntax

Equations

Lean.replaceRef ref oldRef = match Lean.Syntax.getPos? ref with | some x => ref | x => oldRef

source

@[inline]

def Lean.withRef {m : Type → Type} [inst : Monad m] [inst : Lean.MonadRef m] {α : Type} (ref : Lean.Syntax) (x : m α) :

m α

Equations

Lean.withRef ref x = do let oldRef ← Lean.getRef let ref : Lean.Syntax := Lean.replaceRef ref oldRef Lean.MonadRef.withRef ref x

source

class Lean.MonadQuotation (m : Type → Type) extends Lean.MonadRef :

Type 1

getCurrMacroScope : m Lean.MacroScope
getMainModule : m Lean.Name
withFreshMacroScope : {α : Type} → m α → m α

Instances

source

def Lean.MonadRef.mkInfoFromRefPos {m : Type → Type} [inst : Monad m] [inst : Lean.MonadRef m] :

m Lean.SourceInfo

Equations

Lean.MonadRef.mkInfoFromRefPos = do let a ← Lean.getRef pure (Lean.SourceInfo.fromRef a)

source

instance Lean.instMonadQuotation {m : Type → Type} {n : Type → Type} [inst : MonadFunctor m n] [inst : MonadLift m n] [inst : Lean.MonadQuotation m] :

Lean.MonadQuotation n

Equations

Lean.instMonadQuotation = Lean.MonadQuotation.mk (liftM Lean.getCurrMacroScope) (liftM Lean.getMainModule) fun {α} => monadMap fun {β} => Lean.withFreshMacroScope

source

def Lean.Name.hasMacroScopes :

Lean.Name → Bool

Equations

Lean.Name.hasMacroScopes (Lean.Name.str x_1 s x_2) = (s == "_hyg")
Lean.Name.hasMacroScopes (Lean.Name.num p x_1 x_2) = Lean.Name.hasMacroScopes p
Lean.Name.hasMacroScopes x = false

source

def Lean.Name.eraseMacroScopes (n : Lean.Name) :

Lean.Name

Equations

Lean.Name.eraseMacroScopes n = match Lean.Name.hasMacroScopes n with | true => Lean.eraseMacroScopesAux n | false => n

source

def Lean.Name.simpMacroScopes (n : Lean.Name) :

Lean.Name

Equations

Lean.Name.simpMacroScopes n = match Lean.Name.hasMacroScopes n with | true => Lean.simpMacroScopesAux n | false => n

source

structure Lean.MacroScopesView :

Type

name : Lean.Name
imported : Lean.Name
mainModule : Lean.Name
scopes : List Lean.MacroScope

source

instance Lean.instInhabitedMacroScopesView :

Inhabited Lean.MacroScopesView

Equations

Lean.instInhabitedMacroScopesView = { default := { name := default, imported := default, mainModule := default, scopes := default } }

source

def Lean.MacroScopesView.review (view : Lean.MacroScopesView) :

Lean.Name

Equations

Lean.MacroScopesView.review view = match view.scopes with | [] => view.name | x :: x_1 => let base := Lean.Name.mkStr (Lean.Name.mkStr view.name "_@" ++ view.imported ++ view.mainModule) "_hyg"; List.foldl Lean.Name.mkNum base view.scopes

source

def Lean.extractMacroScopes (n : Lean.Name) :

Lean.MacroScopesView

Equations

Lean.extractMacroScopes n = match Lean.Name.hasMacroScopes n with | true => Lean.extractMacroScopesAux n [] | false => { name := n, imported := Lean.Name.anonymous, mainModule := Lean.Name.anonymous, scopes := [] }

source

def Lean.addMacroScope (mainModule : Lean.Name) (n : Lean.Name) (scp : Lean.MacroScope) :

Lean.Name

Equations

Lean.addMacroScope mainModule n scp = match Lean.Name.hasMacroScopes n with | true => let view := Lean.extractMacroScopes n; match view.mainModule == mainModule with | true => Lean.Name.mkNum n scp | false => Lean.MacroScopesView.review { name := view.name, imported := List.foldl Lean.Name.mkNum (view.imported ++ view.mainModule) view.scopes, mainModule := mainModule, scopes := [scp] } | false => Lean.Name.mkNum (Lean.Name.mkStr (Lean.Name.mkStr n "_@" ++ mainModule) "_hyg") scp

source

@[inline]

def Lean.MonadQuotation.addMacroScope {m : Type → Type} [inst : Lean.MonadQuotation m] [inst : Monad m] (n : Lean.Name) :

m Lean.Name

Equations

Lean.MonadQuotation.addMacroScope n = do let mainModule ← Lean.getMainModule let scp ← Lean.getCurrMacroScope pure (Lean.addMacroScope mainModule n scp)

source

def Lean.defaultMaxRecDepth :

Nat

Equations

Lean.defaultMaxRecDepth = 512

source

def Lean.maxRecDepthErrorMessage :

String

Equations

Lean.maxRecDepthErrorMessage = "maximum recursion depth has been reached (use `set_option maxRecDepth ` to increase limit)"

source

noncomputable instance Lean.Macro.instNonemptyMethodsRef :

Nonempty Lean.Macro.MethodsRef

Equations

Lean.Macro.instNonemptyMethodsRef = Lean.Macro.instNonemptyMethodsRef.proof_1

source

structure Lean.Macro.Context :

Type

methods : Lean.Macro.MethodsRef
mainModule : Lean.Name
currMacroScope : Lean.MacroScope
currRecDepth : Nat
maxRecDepth : Nat
ref : Lean.Syntax

source

inductive Lean.Macro.Exception :

Type

error: Lean.Syntax → String → Lean.Macro.Exception
unsupportedSyntax: Lean.Macro.Exception

source

structure Lean.Macro.State :

Type

macroScope : Lean.MacroScope
traceMsgs : List (Lean.Name × String)

source

instance Lean.Macro.instInhabitedState :

Inhabited Lean.Macro.State

Equations

Lean.Macro.instInhabitedState = { default := { macroScope := default, traceMsgs := default } }

source

@[inline]

abbrev Lean.MacroM (α : Type) :

Type

Equations

Lean.MacroM = ReaderT Lean.Macro.Context (EStateM Lean.Macro.Exception Lean.Macro.State)

source

@[inline]

abbrev Lean.Macro :

Type

Equations

Lean.Macro = (Lean.Syntax → Lean.MacroM Lean.Syntax)

source

instance Lean.Macro.instMonadRefMacroM :

Lean.MonadRef Lean.MacroM

Equations

Lean.Macro.instMonadRefMacroM = { getRef := do let ctx ← read pure ctx.ref, withRef := fun {α} ref x => withReader (fun ctx => { methods := ctx.methods, mainModule := ctx.mainModule, currMacroScope := ctx.currMacroScope, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ref }) x }

source

def Lean.Macro.addMacroScope (n : Lean.Name) :

Lean.MacroM Lean.Name

Equations

Lean.Macro.addMacroScope n = do let ctx ← read pure (Lean.addMacroScope ctx.mainModule n ctx.currMacroScope)

source

def Lean.Macro.throwUnsupported {α : Type} :

Lean.MacroM α

Equations

Lean.Macro.throwUnsupported = throw Lean.Macro.Exception.unsupportedSyntax

source

def Lean.Macro.throwError {α : Type} (msg : String) :

Lean.MacroM α

Equations

Lean.Macro.throwError msg = do let ref ← Lean.getRef throw (Lean.Macro.Exception.error ref msg)

source

def Lean.Macro.throwErrorAt {α : Type} (ref : Lean.Syntax) (msg : String) :

Lean.MacroM α

Equations

Lean.Macro.throwErrorAt ref msg = Lean.withRef ref (Lean.Macro.throwError msg)

source

@[inline]

def Lean.Macro.withFreshMacroScope {α : Type} (x : Lean.MacroM α) :

Lean.MacroM α

Equations

Lean.Macro.withFreshMacroScope x = do let fresh ← modifyGet fun s => (s.macroScope, { macroScope := s.macroScope + 1, traceMsgs := s.traceMsgs }) withReader (fun ctx => { methods := ctx.methods, mainModule := ctx.mainModule, currMacroScope := fresh, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref }) x

source

@[inline]

def Lean.Macro.withIncRecDepth {α : Type} (ref : Lean.Syntax) (x : Lean.MacroM α) :

Lean.MacroM α

Equations

Lean.Macro.withIncRecDepth ref x = do let ctx ← read match ctx.currRecDepth == ctx.maxRecDepth with | true => throw (Lean.Macro.Exception.error ref Lean.maxRecDepthErrorMessage) | false => withReader (fun ctx => { methods := ctx.methods, mainModule := ctx.mainModule, currMacroScope := ctx.currMacroScope, currRecDepth := ctx.currRecDepth + 1, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref }) x

source

instance Lean.Macro.instMonadQuotationMacroM :

Lean.MonadQuotation Lean.MacroM

Equations

Lean.Macro.instMonadQuotationMacroM = Lean.MonadQuotation.mk (fun ctx => pure ctx.currMacroScope) (fun ctx => pure ctx.mainModule) fun {α} => Lean.Macro.withFreshMacroScope

source

structure Lean.Macro.Methods :

Type

expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
getCurrNamespace : Lean.MacroM Lean.Name
hasDecl : Lean.Name → Lean.MacroM Bool
resolveNamespace? : Lean.Name → Lean.MacroM (Option Lean.Name)
resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))

source

instance Lean.Macro.instInhabitedMethods :

Inhabited Lean.Macro.Methods

Equations

Lean.Macro.instInhabitedMethods = { default := { expandMacro? := default, getCurrNamespace := default, hasDecl := default, resolveNamespace? := default, resolveGlobalName := default } }