Init.Prelude

An abbreviation for PUnit.{0}, its most common instantiation. This Type should be preferred over PUnit where possible to avoid unnecessary universe parameters.

source

@[matchPattern, inline]

abbrev Unit.unit :

Unit

Equations

() = PUnit.unit

source

unsafe axiom lcProof {α : Prop} :

α

Auxiliary unsafe constant used by the Compiler when erasing proofs from code.

source

unsafe axiom lcUnreachable {α : Sort u} :

α

Auxiliary unsafe constant used by the Compiler to mark unreachable code.

source

inductive True :

Prop

intro: True

source

inductive False :

Prop

source

inductive Empty :

Type

source

inductive PEmpty :

Sort u

source

noncomputable def Not (a : Prop) :

Prop

Equations

(¬a) = (a → False)

source

@[macroInline]

def False.elim {C : Sort u} (h : False) :

C

Equations

False.elim h = False.rec (fun x => C) h

source

@[macroInline]

def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) :

b

Equations

absurd h₁ h₂ = False.elim (h₂ h₁)

source

inductive Eq {α : Sort u_1} :

α → α → Prop

refl: ∀ {α : Sort u_1} (a : α), a = a

source

@[matchPattern]

noncomputable def rfl {α : Sort u} {a : α} :

a = a

Equations

@rfl = @rfl.proof_1

source

@[simp]

theorem id_eq {α : Sort u_1} (a : α) :

id a = a

source

theorem Eq.subst {α : Sort u} {motive : α → Prop} {a : α} {b : α} (h₁ : a = b) (h₂ : motive a) :

motive b

source

theorem Eq.symm {α : Sort u} {a : α} {b : α} (h : a = b) :

b = a

source

theorem Eq.trans {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b = c) :

a = c

source

@[macroInline]

def cast {α : Sort u} {β : Sort u} (h : α = β) (a : α) :

β

Equations

cast h a = h ▸ a

source

theorem congrArg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂) :

f a₁ = f a₂

source

theorem congr {α : Sort u} {β : Sort v} {f₁ : α → β} {f₂ : α → β} {a₁ : α} {a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) :

f₁ a₁ = f₂ a₂

source

theorem congrFun {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : f = g) (a : α) :

f a = g a

source

inductive HEq {α : Sort u} :

α → {β : Sort u} → β → Prop

refl: ∀ {α : Sort u} (a : α), HEq a a

source

@[matchPattern]

noncomputable def HEq.rfl {α : Sort u} {a : α} :

HEq a a

Equations

@HEq.rfl = @HEq.rfl.proof_1

source

theorem eq_of_heq {α : Sort u} {a : α} {a' : α} (h : HEq a a') :

a = a'

source

@[unbox]

structure Prod (α : Type u) (β : Type v) :

Type (max u v)

fst : α
snd : β

source

structure PProd (α : Sort u) (β : Sort v) :

Sort (max (max 1 u) v)

fst : α
snd : β

Similar to Prod, but α and β can be propositions. We use this Type internally to automatically generate the brecOn recursor.

source

structure MProd (α : Type u) (β : Type u) :

Type u

fst : α
snd : β

Similar to Prod, but α and β are in the same universe.

source

structure And (a : Prop) (b : Prop) :

Prop

intro :: (

left : a
right : b

)

source

inductive Or (a : Prop) (b : Prop) :

Prop

inl: ∀ {a b : Prop}, a → a ∨ b
inr: ∀ {a b : Prop}, b → a ∨ b

source

theorem Or.intro_left {a : Prop} (b : Prop) (h : a) :

a ∨ b

source

theorem Or.intro_right {b : Prop} (a : Prop) (h : b) :

a ∨ b

source

theorem Or.elim {a : Prop} {b : Prop} {c : Prop} (h : a ∨ b) (left : a → c) (right : b → c) :

c

source

inductive Bool :

Type

false: Bool
true: Bool

source

structure Subtype {α : Sort u} (p : α → Prop) :

Sort (max 1 u)

val : α
property : p val

source

noncomputable def optParam (α : Sort u) (default : α) :

Sort u

Equations

optParam α default = α

Gadget for optional parameter support.

source

noncomputable def outParam (α : Sort u) :

Sort u

Equations

outParam α = α

Gadget for marking output parameters in type classes.

source

def typedExpr (α : Sort u) (a : α) :

α

Equations

typedExpr α a = a

Auxiliary Declaration used to implement the notation (a : α)

source

def namedPattern {α : Sort u} (x : α) (a : α) (h : x = a) :

α

Equations

namedPattern x a h = a

Auxiliary Declaration used to implement the named patterns x@h:p

source

@[neverExtract, extern lean_sorry]

axiom sorryAx (α : Sort u) (synthetic : optParam Bool false) :

α

source

theorem eq_false_of_ne_true {b : Bool} :

¬b = true → b = false

source

theorem eq_true_of_ne_false {b : Bool} :

¬b = false → b = true

source

theorem ne_false_of_eq_true {b : Bool} :

b = true → ¬b = false

source

theorem ne_true_of_eq_false {b : Bool} :

b = false → ¬b = true

source

@[nospecialize]

class Inhabited (α : Sort u) :

Sort (max 1 u)

default : α

Instances

source

class inductive Nonempty (α : Sort u) :

Prop

intro: ∀ {α : Sort u}, α → Nonempty α

Instances

source

axiom Classical.choice {α : Sort u} :

Nonempty α → α

source

noncomputable def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) :

p

Equations

@Nonempty.elim = @Nonempty.elim.proof_1

source

noncomputable instance instNonempty {α : Sort u} [inst : Inhabited α] :

Nonempty α

Equations

@instNonempty = @instNonempty.proof_1

source

noncomputable def Classical.ofNonempty {α : Sort u} [inst : Nonempty α] :

α

Equations

Classical.ofNonempty = Classical.choice (_ : Nonempty α)

source

noncomputable instance instNonemptyForAll (α : Sort u) {β : Sort v} [inst : Nonempty β] :

Nonempty (α → β)

Equations

instNonemptyForAll = instNonemptyForAll.proof_1

source

noncomputable instance instNonemptyForAll_1 (α : Sort u) {β : α → Sort v} [inst : ∀ (a : α), Nonempty (β a)] :

Nonempty ((a : α) → β a)

Equations

instNonemptyForAll_1 = instNonemptyForAll_1.proof_1

source

instance instInhabitedSort :

Inhabited (Sort u)

Equations

instInhabitedSort = { default := PUnit }

source

instance instInhabitedForAll (α : Sort u) {β : Sort v} [inst : Inhabited β] :

Inhabited (α → β)

Equations

instInhabitedForAll α = { default := fun x => default }

source

instance instInhabitedForAll_1 (α : Sort u) {β : α → Sort v} [inst : (a : α) → Inhabited (β a)] :

Inhabited ((a : α) → β a)

Equations

instInhabitedForAll_1 α = { default := fun x => default }

source

instance instInhabitedBool :

Inhabited Bool

Equations

instInhabitedBool = { default := false }

source

structure PLift (α : Sort u) :

Type u

up :: (

down : α

)

Universe lifting operation from Sort to Type

source

theorem PLift.up_down {α : Sort u} (b : PLift α) :

{ down := b.down } = b

source

theorem PLift.down_up {α : Sort u} (a : α) :

{ down := a }.down = a

source

noncomputable def NonemptyType :

Type (u + 1)

Equations

NonemptyType = { α // Nonempty α }

source

@[inline]

abbrev NonemptyType.type (type : NonemptyType) :

Type u

Equations

NonemptyType.type type = type.val

source

instance instInhabitedNonemptyType :

Inhabited NonemptyType

Equations

instInhabitedNonemptyType = { default := { val := PUnit, property := (_ : Nonempty PUnit) } }

source

structure ULift (α : Type s) :

Type (max s r)

up :: (

down : α

)

Universe lifting operation

source

theorem ULift.up_down {α : Type u} (b : ULift α) :

{ down := b.down } = b

source

theorem ULift.down_up {α : Type u} (a : α) :

{ down := a }.down = a

source

class inductive Decidable (p : Prop) :

Type

isFalse: {p : Prop} → ¬p → Decidable p
isTrue: {p : Prop} → p → Decidable p

Instances

source

@[inlineIfReduce, nospecialize]

def Decidable.decide (p : Prop) [h : Decidable p] :

Bool

Equations

decide p = Decidable.casesOn h (fun x => false) fun x => true

source

@[inline]

abbrev DecidablePred {α : Sort u} (r : α → Prop) :

Sort (max 1 u)

Equations

DecidablePred r = ((a : α) → Decidable (r a))

source

@[inline]

abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :

Sort (max 1 u)

Equations

DecidableRel r = ((a b : α) → Decidable (r a b))

source

@[inline]

abbrev DecidableEq (α : Sort u) :

Sort (max 1 u)

Equations

DecidableEq α = ((a b : α) → Decidable (a = b))

source

def decEq {α : Sort u} [s : DecidableEq α] (a : α) (b : α) :

Decidable (a = b)

Equations

decEq a b = s a b

source

theorem decide_eq_true {p : Prop} [s : Decidable p] :

p → decide p = true

source

theorem decide_eq_false {p : Prop} [inst : Decidable p] :

¬p → decide p = false

source

theorem of_decide_eq_true {p : Prop} [s : Decidable p] :

decide p = true → p

source

theorem of_decide_eq_false {p : Prop} [s : Decidable p] :

decide p = false → ¬p

source

theorem of_decide_eq_self_eq_true {α : Sort u_1} [s : DecidableEq α] (a : α) :

decide (a = a) = true

source

@[inline]

instance instDecidableEqBool :

DecidableEq Bool

Equations

instDecidableEqBool a b = match a, b with | false, false => isTrue (_ : false = false) | false, true => isFalse instDecidableEqBool.proof_1 | true, false => isFalse instDecidableEqBool.proof_2 | true, true => isTrue (_ : true = true)

source

instance instBEq {α : Type u_1} [inst : DecidableEq α] :

BEq α

Equations

instBEq = { beq := fun a b => decide (a = b) }

source

@[macroInline]

def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : ¬c → α) :

α

Equations

dite c t e = Decidable.casesOn h e t

source

@[macroInline]

def ite {α : Sort u} (c : Prop) [h : Decidable c] (t : α) (e : α) :

α

Equations

(if c then t else e) = Decidable.casesOn h (fun x => e) fun x => t

source

@[macroInline]

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

Decidable (p ∧ q)

Equations

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

(!_fun_discr) = match _fun_discr 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) :

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

Transitive chaining of proofs, used e.g. by calc.

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

source

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

Type (max (max u v) w)

hSub : α → β → γ

Instances

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

class Membership (α : outParam (Type u)) (γ : Type v) :

Type (max u v)

mem : α → γ → Prop

Instances

source

@[matchPattern, extern lean_nat_add]

def Nat.add :

Nat → Nat → Nat

Equations

Nat.add _fun_discr Nat.zero = _fun_discr
Nat.add _fun_discr (Nat.succ b) = Nat.succ (Nat.add _fun_discr 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 _fun_discr 0 = 0
Nat.mul _fun_discr (Nat.succ b) = Nat.add (Nat.mul _fun_discr b) _fun_discr

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 n) = false
Nat.beq (Nat.succ n) Nat.zero = false
Nat.beq (Nat.succ n) (Nat.succ m) = Nat.beq n m

source

instance instBEqNat :

BEq Nat

Equations

instBEqNat = { beq := Nat.beq }

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 with | true => isTrue (_ : n = m) | false => 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 n) = 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

@[simp]

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

@[simp]

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 _fun_discr = match _fun_discr 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

@[simp]

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 _fun_discr 0 = _fun_discr
Nat.sub _fun_discr (Nat.succ b) = Nat.pred (Nat.sub _fun_discr 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

The Char Type represents an unicode scalar value. See http://www.unicode.org/glossary/#unicode_scalar_value).

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 _fun_discr _fun_discr = match _fun_discr, _fun_discr 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 (head :: tail) [] = isFalse (_ : head :: tail = [] → List.noConfusionType False (head :: tail) [])
List.hasDecEq [] (head :: tail) = isFalse (_ : [] = head :: tail → List.noConfusionType False [] (head :: tail))
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 _fun_discr [] = _fun_discr
List.foldl f _fun_discr (b :: l) = List.foldl f (f _fun_discr b) l

source

def List.set {α : Type u_1} :

List α → Nat → α → List α

Equations

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

source

def List.length {α : Type u_1} :

List α → Nat

Equations

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

source

def List.lengthTRAux {α : Type u_1} :

List α → Nat → Nat

Equations

List.lengthTRAux [] _fun_discr = _fun_discr
List.lengthTRAux (head :: as) _fun_discr = List.lengthTRAux as (Nat.succ _fun_discr)

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 [] _fun_discr = [_fun_discr]
List.concat (a :: as) _fun_discr = a :: List.concat as _fun_discr

source

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

Fin (List.length as) → α

Equations

List.get (a :: tail) { val := 0, isLt := isLt } = a
List.get (head :: as) { val := Nat.succ i, isLt := h } = List.get as { val := i, isLt := (_ : Nat.succ i ≤ 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

structure String.Pos :

Type

byteIdx : Nat

A byte position in a String. Internally, Strings are UTF-8 encoded. Codepoint positions (counting the Unicode codepoints rather than bytes) are represented by plain Nats instead. Indexing a String by a byte position is constant-time, while codepoint positions need to be translated internally to byte positions in linear-time.

source

instance instInhabitedPos :

Inhabited String.Pos

Equations

instInhabitedPos = { default := { byteIdx := 0 } }

source

instance instDecidableEqPos :

DecidableEq String.Pos

Equations

instDecidableEqPos x x = match x with | { byteIdx := a } => match x with | { byteIdx := b } => match decEq a b with | isTrue h => isTrue (_ : { byteIdx := a } = { byteIdx := b }) | isFalse h => isFalse (_ : { byteIdx := a } = { byteIdx := b } → False)

source

structure Substring :

Type

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

source

instance instInhabitedSubstring :

Inhabited Substring

Equations

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

source

@[inline]

def Substring.bsize :

Substring → Nat

Equations

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

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 _fun_discr = match _fun_discr with | { data := s } => String.utf8ByteSize.go s

source

def String.utf8ByteSize.go :

List Char → Nat

Equations

String.utf8ByteSize.go [] = 0
String.utf8ByteSize.go (c :: cs) = String.utf8ByteSize.go cs + String.csize c

source

instance instHAddPos :

HAdd String.Pos String.Pos String.Pos

Equations

instHAddPos = { hAdd := fun p₁ p₂ => { byteIdx := p₁.byteIdx + p₂.byteIdx } }

source

instance instHSubPos :

HSub String.Pos String.Pos String.Pos

Equations

instHSubPos = { hSub := fun p₁ p₂ => { byteIdx := p₁.byteIdx - p₂.byteIdx } }

source

instance instHAddPosChar :

HAdd String.Pos Char String.Pos

Equations

instHAddPosChar = { hAdd := fun p c => { byteIdx := p.byteIdx + String.csize c } }

source

instance instHAddPosString :

HAdd String.Pos String String.Pos

Equations

instHAddPosString = { hAdd := fun p s => { byteIdx := p.byteIdx + String.utf8ByteSize s } }

source

instance instLEPos :

LE String.Pos

Equations

instLEPos = { le := fun p₁ p₂ => p₁.byteIdx ≤ p₂.byteIdx }

source

instance instLTPos :

LT String.Pos

Equations

instLTPos = { lt := fun p₁ p₂ => p₁.byteIdx < p₂.byteIdx }

source

instance instDecidableLePosInstLEPos (p₁ : String.Pos) (p₂ : String.Pos) :

Decidable (p₁ ≤ p₂)

Equations

instDecidableLePosInstLEPos p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx ≤ p₂.byteIdx))

source

instance instDecidableLtPosInstLTPos (p₁ : String.Pos) (p₂ : String.Pos) :

Decidable (p₁ < p₂)

Equations

instDecidableLtPosInstLTPos p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))

source

@[inline]

def String.endPos (s : String) :

String.Pos

Equations

String.endPos s = { byteIdx := String.utf8ByteSize s }

source

@[inline]

def String.toSubstring (s : String) :

Substring

Equations

String.toSubstring s = { str := s, startPos := { byteIdx := 0 }, stopPos := String.endPos 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

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 = Array.appendCore.loop bs (Array.size bs) 0 as

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 [] _fun_discr = _fun_discr
List.toArrayAux (a :: as) _fun_discr = List.toArrayAux as (Array.push _fun_discr a)

source

@[inlineIfReduce]

def List.redLength {α : Type u_1} :

List α → Nat

Equations

List.redLength [] = 0
List.redLength (head :: 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

class Monad (m : Type u → Type v) extends Applicative , Bind :

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 = Array.sequenceMap.loop as f (Array.size as) 0 Array.empty

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 α

A Function for lifting a computation from an inner Monad to an outer Monad. Like MonadTrans, but n does not have to be a monad transformer. Alternatively, an implementation of MonadLayer without layerInvmap (so far).

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 α

The reflexive-transitive closure of MonadLift. monadLift is used to transitively lift monadic computations such as StateT.get or StateT.puts. Corresponds to MonadLift.

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 α

A functor in the category of monads. Can be used to lift monad-transforming functions. Based on pipes' MFunctor, but not restricted to monad transformers. Alternatively, an implementation of MonadTransFunctor.

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 α

The reflexive-transitive closure of MonadFunctor. monadMap is used to transitively lift Monad morphisms

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 α

An implementation of MonadError

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 α

Similar to MonadExceptOf, but ε is an outParam for convenience

Instances

instMonadExcept

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 α)

An implementation of ReaderT

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 x = 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 ρ

An implementation of MonadReader. It does not contain local because this Function cannot be lifted using monadLift. Instead, the MonadReaderAdapter class provides the more general adaptReader Function.

Note: This class can be seen as a simplification of the more "principled" definition
```
class MonadReader (ρ : outParam (Type u)) (n : Type u → Type u) where
  lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α
```

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 ρ

Similar to MonadReaderOf, but ρ is an outParam for convenience

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 α

An implementation of MonadState. In contrast to the Haskell implementation, we use overlapping instances to derive instances automatically from monadLift.

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 α

Similar to MonadStateOf, but σ is an outParam for convenience

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 : σ → δ → σ

Auxiliary instance for saving/restoring the "backtrackable" part of the state.

Instances

EStateM.nonBacktrackable

source

@[inline]

def EStateM.tryCatch {ε : Type u} {σ : Type u} {δ : 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} {δ : 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 a 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 a 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} {δ : 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} {δ : 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 a => some v | EStateM.Result.error a a_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 _fun_discr = match _fun_discr with | Lean.Name.anonymous => UInt64.ofNatCore 1723 Lean.Name.hash.proof_1 | Lean.Name.str a a_1 h => h | Lean.Name.num a a_1 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₁ a) (Lean.Name.str p₂ s₂ a_1) = (s₁ == s₂ && Lean.Name.beq p₁ p₂)
Lean.Name.beq (Lean.Name.num p₁ n₁ a) (Lean.Name.num p₂ n₂ a_1) = (n₁ == n₂ && Lean.Name.beq p₁ p₂)
Lean.Name.beq _fun_discr _fun_discr = 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 _fun_discr Lean.Name.anonymous = _fun_discr
Lean.Name.append _fun_discr (Lean.Name.str p s a) = Lean.Name.mkStr (Lean.Name.append _fun_discr p) s
Lean.Name.append _fun_discr (Lean.Name.num p d a) = Lean.Name.mkNum (Lean.Name.append _fun_discr 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 information of tokens.

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 leading pos trailing endPos, x => some pos | Lean.SourceInfo.synthetic pos endPos, 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

Syntax objects used by the parser, macro expander, delaborator, etc.

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 = `str

source

def Lean.charLitKind :

Lean.SyntaxNodeKind

Equations

Lean.charLitKind = `char

source

def Lean.numLitKind :

Lean.SyntaxNodeKind

Equations

Lean.numLitKind = `num

source

def Lean.scientificLitKind :

Lean.SyntaxNodeKind

Equations

Lean.scientificLitKind = `scientific

source

def Lean.nameLitKind :

Lean.SyntaxNodeKind

Equations

Lean.nameLitKind = `name

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 info k args => k | Lean.Syntax.missing => `missing | Lean.Syntax.atom info v => Lean.Name.mkSimple v | Lean.Syntax.ident info rawVal val preresolved => 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 kind 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 info kind 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 info kind 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 info kind args => Array.size args | x => 0

source

def Lean.Syntax.isMissing :

Lean.Syntax → Bool

Equations

Lean.Syntax.isMissing _fun_discr = match _fun_discr 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 _fun_discr = match _fun_discr with | Lean.Syntax.ident info rawVal val preresolved => true | x => false

source

def Lean.Syntax.getId :

Lean.Syntax → Lean.Name

Equations

Lean.Syntax.getId _fun_discr = match _fun_discr with | Lean.Syntax.ident info rawVal val preresolved => val | x => Lean.Name.anonymous

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 args => 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

Retrieve the left-most node or leaf's info in the Syntax tree.

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

Retrieve the left-most leaf's info in the Syntax tree, or none if there is no token.

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

An array of syntax elements interspersed with separators. Can be coerced to/from ArraySyntax to automatically remove/insert the separators.

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

Macro scope used internally. It is not available for our frontend.

source

def Lean.firstFrontendMacroScope :

Nat

Equations

Lean.firstFrontendMacroScope = Lean.reservedMacroScope + 1

First macro scope available for our frontend

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 val => 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 α

A monad that supports syntax quotations. Syntax quotations (in term position) are monadic values that when executed retrieve the current "macro scope" from the monad and apply it to every identifier they introduce (independent of whether this identifier turns out to be a reference to an existing declaration, or an actually fresh binding during further elaboration). We also apply the position of the result of getRef to each introduced symbol, which results in better error positions than not applying any position.

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 a s a_1) = (s == "_hyg")
Lean.Name.hasMacroScopes (Lean.Name.num p a a_1) = Lean.Name.hasMacroScopes p
Lean.Name.hasMacroScopes _fun_discr = 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 | head :: tail => 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 := [] }

Revert all addMacroScope calls. v=extractMacroScopesn→n=v.review. This operation is useful for analyzing/transforming the original identifiers, then adding back the scopes (via MacroScopesView.review).

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

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.Name.eraseMacroScopes (Lean.Syntax.getId stx) == Lean.Name.eraseMacroScopes id)

Function used for determining whether a syntax pattern `(id) is matched. There are various conceivable notions of when two syntactic identifiers should be regarded as identical, but semantic definitions like whether they refer to the same global name cannot be implemented without context information (i.e. MonadResolveName). Thus in patterns we default to the structural solution of comparing the identifiers' Name values, though we at least do so modulo macro scopes so that identifiers that "look" the same match. This is particularly useful when dealing with identifiers that do not actually refer to Lean bindings, e.g. in the stx pattern `(many($p)).

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 info k' args => k == k' && match Array.getD args 0 Lean.Syntax.missing with | Lean.Syntax.atom info val' => val == val' | x => false | x => false

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 } }

source

unsafe def Lean.Macro.mkMethodsImp (methods : Lean.Macro.Methods) :

Lean.Macro.MethodsRef

Equations

Lean.Macro.mkMethodsImp methods = unsafeCast methods

source

@[implementedBy Lean.Macro.mkMethodsImp]

constant Lean.Macro.mkMethods (methods : Lean.Macro.Methods) :

Lean.Macro.MethodsRef

source

instance Lean.Macro.instInhabitedMethodsRef :

Inhabited Lean.Macro.MethodsRef

Equations

Lean.Macro.instInhabitedMethodsRef = { default := Lean.Macro.mkMethods default }

source

unsafe def Lean.Macro.getMethodsImp :

Lean.MacroM Lean.Macro.Methods

Equations

Lean.Macro.getMethodsImp = do let ctx ← read pure (unsafeCast ctx.methods)

source

@[implementedBy Lean.Macro.getMethodsImp]

constant Lean.Macro.getMethods :

Lean.MacroM Lean.Macro.Methods

source

def Lean.Macro.expandMacro? (stx : Lean.Syntax) :

Lean.MacroM (Option Lean.Syntax)

Equations

Lean.expandMacro? stx = do let a ← Lean.Macro.getMethods Lean.Macro.Methods.expandMacro? a stx

expandMacro?stx return somestxNew if stx is a macro, and stxNew is its expansion.

source

def Lean.Macro.hasDecl (declName : Lean.Name) :

Lean.MacroM Bool

Equations

Lean.Macro.hasDecl declName = do let a ← Lean.Macro.getMethods Lean.Macro.Methods.hasDecl a declName

Return true if the environment contains a declaration with name declName

source

def Lean.Macro.getCurrNamespace :

Lean.MacroM Lean.Name

Equations

Lean.Macro.getCurrNamespace = do let a ← Lean.Macro.getMethods a.getCurrNamespace

source

def Lean.Macro.resolveNamespace? (n : Lean.Name) :

Lean.MacroM (Option Lean.Name)

Equations

Lean.Macro.resolveNamespace? n = do let a ← Lean.Macro.getMethods Lean.Macro.Methods.resolveNamespace? a n

source

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

Lean.MacroM (List (Lean.Name × List String))

Equations

Lean.Macro.resolveGlobalName n = do let a ← Lean.Macro.getMethods Lean.Macro.Methods.resolveGlobalName a n

source

def Lean.Macro.trace (clsName : Lean.Name) (msg : String) :

Lean.MacroM Unit

Equations

Lean.Macro.trace clsName msg = modify fun s => { macroScope := s.macroScope, traceMsgs := (clsName, msg) :: s.traceMsgs }

source

@[inline]

abbrev Lean.PrettyPrinter.UnexpandM (α : Type) :

Type

Equations

Lean.PrettyPrinter.UnexpandM = ReaderT Lean.Syntax (EStateM Unit Unit)

source

@[inline]

abbrev Lean.PrettyPrinter.Unexpander :

Type

Equations

Lean.PrettyPrinter.Unexpander = (Lean.Syntax → Lean.PrettyPrinter.UnexpandM Lean.Syntax)

Function that tries to reverse macro expansions as a post-processing step of delaboration. While less general than an arbitrary delaborator, it can be declared without importing Lean. Used by the [appUnexpander] attribute.

source

instance Lean.PrettyPrinter.instMonadQuotationUnexpandM :

Lean.MonadQuotation Lean.PrettyPrinter.UnexpandM

Equations

Lean.PrettyPrinter.instMonadQuotationUnexpandM = Lean.MonadQuotation.mk (pure 0) (pure `_fakeMod) fun {α} => id