structure Isotope.STm.Lang (Arity : Type uargs) [I : Args Arity] : Type (max (max uargs (uop + 1)) (uval + 1))

• Val : Type uval
• Op : Arity → Type uop

inductive Isotope.STm {Arity : Type u_1} [I : Args Arity] (L : STm.Lang Arity) (A : Type uatom) : Type (max (max (max (max u_1 u_2) u_3) u_4) uatom)

• sym {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} : A → STm L A
• const {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} : L.Val → STm L A
• op {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} {arity : Arity} : L.Op arity → (UArgs.Ix arity → STm L A) → STm L A

inductive Isotope.STm.Lang.Tag {Arity : Type u_1} [I : Args Arity] (L : Lang Arity) : Type (max (max u_1 u_3) u_4)

• val {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} : L.Val → L.Tag
• op {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {arity : Arity} (o : L.Op arity) : L.Tag

def Isotope.STm.Lang.Tag.arity? {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} : L.Tag → WithZero Arity

Equations

• (Isotope.STm.Lang.Tag.val a).arity? = 0
• (Isotope.STm.Lang.Tag.op o).arity? = ↑arity

inductive Isotope.STm.Lang.Tag? {Arity : Type u_1} [I : Args Arity] (L : Lang Arity) (A : Type uatom) : Type (max (max (max u_1 u_3) u_4) uatom)

• sym {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} (a : A) : L.Tag? A
• val {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} (c : L.Val) : L.Tag? A
• op {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} {arity : Arity} (o : L.Op arity) : L.Tag? A

def Isotope.STm.Lang.Tag?.arity? {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type uatom} : L.Tag? A → WithZero Arity

Equations

• (Isotope.STm.Lang.Tag?.op o).arity? = ↑arity
• x✝.arity? = 0

def Isotope.STm.arity? {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} : STm L A → Option Arity

Equations

• (Isotope.STm.op a a_1).arity? = some arity
• x✝.arity? = none

def Isotope.STm.tag? {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} (e : STm L A) : Option L.Tag

Equations

• (Isotope.STm.const c).tag? = some (Isotope.STm.Lang.Tag.val c)
• (Isotope.STm.op o a).tag? = some (Isotope.STm.Lang.Tag.op o)
• x✝.tag? = none

@[implicit_reducible]

instance Isotope.STm.instCoeSym {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} : Coe A (STm L A)

Equations

• Isotope.STm.instCoeSym = { coe := Isotope.STm.sym }

@[implicit_reducible]

instance Isotope.STm.instCoeVal {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} : Coe L.Val (STm L A)

Equations

• Isotope.STm.instCoeVal = { coe := Isotope.STm.const }

@[implicit_reducible]

instance Isotope.STm.instInhabited {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} [Inhabited L.Val] : Inhabited (STm L A)

Equations

• Isotope.STm.instInhabited = { default := Isotope.STm.const default }

instance Isotope.STm.instNonemptySym {Arity : Type u_5} [I : Args Arity] {L : Lang Arity} {A : Type u_1} [inst : Nonempty A] : Nonempty (STm L A)

instance Isotope.STm.instNonemptyVal {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A : Type u_5} [inst : Nonempty L.Val] : Nonempty (STm L A)

def Isotope.STm.mapSym {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A : Type u_5} {A' : Type u_6} (f : A → A') : STm L A → STm L A'

Equations

• Isotope.STm.mapSym f (Isotope.STm.sym a) = Isotope.STm.sym (f a)
• Isotope.STm.mapSym f (Isotope.STm.const c) = Isotope.STm.const c
• Isotope.STm.mapSym f (Isotope.STm.op o es) = Isotope.STm.op o fun (i : Isotope.UArgs.Ix arity) => Isotope.STm.mapSym f (es i)

@[simp]

theorem Isotope.STm.mapSym_id {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A : Type u_1} (e : STm L A) : mapSym id e = e

@[simp]

theorem Isotope.STm.mapSym_mapSym {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ : Type u_1} {A₂ : Type u_7} {A₃ : Type u_6} (f : A₁ → A₂) (g : A₂ → A₃) (e : STm L A₁) : mapSym g (mapSym f e) = mapSym (g ∘ f) e

def Isotope.STm.substSym {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A₁ : Type u_5} {A₂ : Type u_6} (f : A₁ → STm L A₂) : STm L A₁ → STm L A₂

Equations

• Isotope.STm.substSym f (Isotope.STm.sym a) = f a
• Isotope.STm.substSym f (Isotope.STm.const c) = Isotope.STm.const c
• Isotope.STm.substSym f (Isotope.STm.op o es) = Isotope.STm.op o fun (i : Isotope.UArgs.Ix arity) => Isotope.STm.substSym f (es i)

@[simp]

theorem Isotope.STm.substSym_sym_comp {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ : Type u_5} {A₂ : Type u_6} (f : A₁ → A₂) : substSym (sym ∘ f) = mapSym f

@[simp]

theorem Isotope.STm.substSym_sym {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A : Type u_1} (e : STm L A) : substSym sym e = e

@[simp]

theorem Isotope.STm.substSym_substSym {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ : Type u_7} {A₂ : Type u_1} {A₃ : Type u_6} (f : A₁ → STm L A₂) (g : A₂ → STm L A₃) (e : STm L A₁) : substSym g (substSym f e) = substSym (fun (a : A₁) => substSym g (f a)) e

@[implicit_reducible]

instance Isotope.STm.instMonad {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} : Monad (STm L)

Equations

• One or more equations did not get rendered due to their size.

theorem Isotope.STm.map_def {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_1} (f : A₁ → A₂) (e : STm L A₁) : f <$> e = mapSym f e

@[simp]

theorem Isotope.STm.map_sym {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_5} (f : A₁ → A₂) (a : A₁) : f <$> sym a = sym (f a)

@[simp]

theorem Isotope.STm.map_const {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_5} (f : A₁ → A₂) (c : L.Val) : f <$> const c = const c

@[simp]

theorem Isotope.STm.map_op {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_5} (f : A₁ → A₂) {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A₁) : f <$> op o es = op o fun (i : UArgs.Ix arity) => f <$> es i

theorem Isotope.STm.bind_def {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_1} (e : STm L A₁) (f : A₁ → STm L A₂) : e >>= f = substSym f e

@[simp]

theorem Isotope.STm.bind_sym {Arity : Type u_2} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_1} (a : A₁) (f : A₁ → STm L A₂) : sym a >>= f = f a

@[simp]

theorem Isotope.STm.bind_const {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_5} (c : L.Val) (f : A₁ → STm L A₂) : const c >>= f = const c

@[simp]

theorem Isotope.STm.bind_op {Arity : Type u_1} [I : Args Arity] {L : Lang Arity} {A₁ A₂ : Type u_5} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A₁) (f : A₁ → STm L A₂) : op o es >>= f = op o (es >=> f)

instance Isotope.STm.instLawfulMonad {Arity : Type u_5} [I : Args Arity] {L : Lang Arity} : LawfulMonad (STm L)