Documentation

Isotope.SExp.Defs

inductive Isotope.SExp2 (A : Type ua) :

atom {A : Type ua} : A → SExp2 A
pair {A : Type ua} : SExp2 A → SExp2 A → SExp2 A
nil {A : Type ua} : SExp2 A

Instances For

inductive Isotope.SExp (A : Type ua) :

atom {A : Type ua} : A → SExp A
par {A : Type ua} {length : ℕ} : (Fin length → SExp A) → SExp A

Instances For

@[implicit_reducible]

instance Isotope.SExp.instCoe {A : Type ua} :

Coe A (SExp A)

Equations

Isotope.SExp.instCoe = { coe := Isotope.SExp.atom }

def Isotope.SExp.parL {A : Type ua} (es : List (SExp A)) :

Equations

Isotope.SExp.parL es = Isotope.SExp.par es.get

Instances For

def Isotope.SExp.nil {A : Type ua} :

Equations

Isotope.SExp.nil = Isotope.SExp.parL []

Instances For

@[implicit_reducible]

instance Isotope.SExp.instEmptyCollection {A : Type ua} :

EmptyCollection (SExp A)

Equations

Isotope.SExp.instEmptyCollection = { emptyCollection := Isotope.SExp.nil }

@[implicit_reducible]

instance Isotope.SExp.instInhabited {A : Type ua} :

Inhabited (SExp A)

Equations

Isotope.SExp.instInhabited = { default := Isotope.SExp.nil }

theorem Isotope.SExp.nil_def {A : Type ua} :

theorem Isotope.SExp.par_congr {A : Type ua} {length length' : ℕ} (h : length = length') {es : Fin length → SExp A} {es' : Fin length' → SExp A} (hes : ∀ (i : Fin length), es i = es' (Fin.cast h i)) :

par es = par es'

theorem Isotope.SExp.parL_congr {A : Type ua} {es es' : List (SExp A)} (hlength : es.length = es'.length) (helem : ∀ (i : ℕ) (x : i < es.length), es[i] = es'[i]) :

parL es = parL es'

theorem Isotope.SExp.parL_ofFn {A : Type ua} {length : ℕ} (es : Fin length → SExp A) :

parL (List.ofFn es) = par es

theorem Isotope.SExp.par_get {A : Type ua} (es : List (SExp A)) :

par es.get = parL es

inductive Isotope.SExp.ParF (A : Type ua) (X : Type ux) :

Type (max ua ux)

atom {A : Type ua} {X : Type ux} (a : A) : ParF A X
par {A : Type ua} {X : Type ux} {arity : ℕ} (es : Fin arity → X) : ParF A X

Instances For

def Isotope.SExp.unrollF {A : Type ua} :

SExp A → ParF A (SExp A)

Equations

(Isotope.SExp.atom a).unrollF = Isotope.SExp.ParF.atom a
(Isotope.SExp.par es).unrollF = Isotope.SExp.ParF.par es

Instances For

def Isotope.SExp.ParF.roll {A : Type ua} :

ParF A (SExp A) → SExp A

Equations

(Isotope.SExp.ParF.atom a).roll = Isotope.SExp.atom a
(Isotope.SExp.ParF.par es).roll = Isotope.SExp.par es

Instances For

@[simp]

theorem Isotope.SExp.ParF.unroll_roll {A : Type ua} (e : ParF A (SExp A)) :

e.roll.unrollF = e

@[simp]

theorem Isotope.SExp.roll_unrollF {A : Type ua} (e : SExp A) :

e.unrollF.roll = e

inductive Isotope.SExp.ParL (A : Type ua) (X : Type ux) :

Type (max ua ux)

atom {A : Type ua} {X : Type ux} (a : A) : ParL A X
parL {A : Type ua} {X : Type ux} (es : List X) : ParL A X

Instances For

def Isotope.SExp.ParL.roll {A : Type ua} :

ParL A (SExp A) → SExp A

Equations

(Isotope.SExp.ParL.atom a).roll = Isotope.SExp.atom a
(Isotope.SExp.ParL.parL es).roll = Isotope.SExp.parL es

Instances For

def Isotope.SExp.unrollL {A : Type ua} :

SExp A → ParL A (SExp A)

Equations

(Isotope.SExp.atom a).unrollL = Isotope.SExp.ParL.atom a
(Isotope.SExp.par es).unrollL = Isotope.SExp.ParL.parL (List.ofFn es)

Instances For

@[simp]

theorem Isotope.SExp.ParL.unroll_roll {A : Type ua} (e : ParL A (SExp A)) :

e.roll.unrollL = e

@[simp]

theorem Isotope.SExp.roll_unrollL {A : Type ua} (e : SExp A) :

e.unrollL.roll = e

def Isotope.SExp.listInduction {A : Type ua} {motive : SExp A → Sort ui} (atom : (a : A) → motive (atom a)) (parL : (es : List (SExp A)) → ((i : ℕ) → (x : i < es.length) → motive es[i]) → motive (parL es)) (e : SExp A) :

motive e

Equations

One or more equations did not get rendered due to their size.
Isotope.SExp.listInduction atom parL (Isotope.SExp.atom a) = atom a

Instances For

@[implicit_reducible]

instance Isotope.SExp.instDecidableEq {A : Type ua} [DecidableEq A] :

DecidableEq (SExp A)

Equations

One or more equations did not get rendered due to their size.
(Isotope.SExp.atom a).instDecidableEq (Isotope.SExp.atom b) = ⋯.mpr inferInstance
(Isotope.SExp.atom a).instDecidableEq (Isotope.SExp.par a_1) = isFalse ⋯
(Isotope.SExp.par a).instDecidableEq (Isotope.SExp.atom a_1) = isFalse ⋯

def Isotope.SExp.mapAtom {A : Type ua} {A' : Type u_1} (f : A → A') :

SExp A → SExp A'

Equations

Isotope.SExp.mapAtom f (Isotope.SExp.atom a) = Isotope.SExp.atom (f a)
Isotope.SExp.mapAtom f (Isotope.SExp.par es) = Isotope.SExp.par fun (i : Fin length) => Isotope.SExp.mapAtom f (es i)

Instances For

@[simp]

theorem Isotope.SExp.mapAtom_id {A : Type ua} (e : SExp A) :

mapAtom id e = e

@[simp]

theorem Isotope.SExp.mapAtom_mapAtom {A : Type ua} {A' : Type u_2} {A'' : Type u_1} (f : A → A') (g : A' → A'') (e : SExp A) :

mapAtom g (mapAtom f e) = mapAtom (g ∘ f) e

def Isotope.SExp.substAtom {A : Type ua} {A' : Type u_1} (f : A → SExp A') :

SExp A → SExp A'

Equations

Isotope.SExp.substAtom f (Isotope.SExp.atom a) = f a
Isotope.SExp.substAtom f (Isotope.SExp.par es) = Isotope.SExp.par fun (i : Fin length) => Isotope.SExp.substAtom f (es i)

Instances For

@[simp]

theorem Isotope.SExp.substAtom_atom_comp {A : Type ua} {A' : Type u_1} (f : A → A') :

substAtom (atom ∘ f) = mapAtom f

@[simp]

theorem Isotope.SExp.substAtom_atom {A : Type ua} (e : SExp A) :

substAtom atom e = e

@[simp]

theorem Isotope.SExp.substAtom_substAtom {A : Type ua} {A' : Type u_1} {A'' : Type u_2} (f : A → SExp A') (g : A' → SExp A'') (e : SExp A) :

substAtom g (substAtom f e) = substAtom (fun (a : A) => substAtom g (f a)) e

@[simp]

theorem Isotope.SExp.substAtom_parL {A : Type ua} {A' : Type u_1} (f : A → SExp A') (es : List (SExp A)) :

substAtom f (parL es) = parL (List.map (substAtom f) es)

@[simp]

theorem Isotope.SExp.mapAtom_parL {A : Type ua} {A' : Type u_1} (f : A → A') (es : List (SExp A)) :

mapAtom f (parL es) = parL (List.map (mapAtom f) es)

@[simp]

theorem Isotope.SExp.mapAtom_nil {A : Type ua} {A' : Type u_1} (f : A → A') :

mapAtom f ∅ = ∅

@[simp]

theorem Isotope.SExp.substAtom_nil {A : Type ua} {A' : Type u_1} (f : A → SExp A') :

substAtom f ∅ = ∅

@[implicit_reducible]

instance Isotope.SExp.instMonad :

Equations

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

theorem Isotope.SExp.map_def {A A' : Type ua} (f : A → A') (e : SExp A) :

f <$> e = mapAtom f e

@[simp]

theorem Isotope.SExp.map_atom {A A' : Type ua} (f : A → A') (a : A) :

f <$> atom a = atom (f a)

@[simp]

theorem Isotope.SExp.map_par {A A' : Type ua} (f : A → A') {length : ℕ} (es : Fin length → SExp A) :

f <$> par es = par fun (i : Fin length) => f <$> es i

@[simp]

theorem Isotope.SExp.map_parL {A A' : Type ua} (f : A → A') (es : List (SExp A)) :

f <$> parL es = parL (mapAtom f <$> es)

theorem Isotope.SExp.bind_def {A A' : Type ua} (f : A → SExp A') (e : SExp A) :

e >>= f = substAtom f e

@[simp]

theorem Isotope.SExp.bind_atom {A A' : Type ua} (f : A → SExp A') (a : A) :

atom a >>= f = f a

@[simp]

theorem Isotope.SExp.bind_par {A A' : Type ua} (f : A → SExp A') {length : ℕ} (es : Fin length → SExp A) :

par es >>= f = par (es >=> f)

@[simp]

theorem Isotope.SExp.bind_parL {A A' : Type ua} (f : A → SExp A') (es : List (SExp A)) :

parL es >>= f = parL ((fun (e : SExp A) => e >>= f) <$> es)

instance Isotope.SExp.instLawfulMonad :

LawfulMonad SExp

def Isotope.SExp.inlAtom {L : Type u_1} {R : Type u_2} :

SExp L → SExp (L ⊕ R)

Equations

Isotope.SExp.inlAtom = Isotope.SExp.mapAtom Sum.inl

Instances For

def Isotope.SExp.inrAtom {L : Type u_1} {R : Type u_2} :

SExp R → SExp (L ⊕ R)

Equations

Isotope.SExp.inrAtom = Isotope.SExp.mapAtom Sum.inr

Instances For

def Isotope.SExp.cswapAtom {L : Type u_1} {R : Type u_2} :

SExp (L ⊕ R) → SExp (R ⊕ L)

Equations

Isotope.SExp.cswapAtom = Isotope.SExp.mapAtom Sum.swap

Instances For

def Isotope.SExp.fstAtom {L : Type u_1} {R : Type u_2} :

SExp (L × R) → SExp L

Equations

Isotope.SExp.fstAtom = Isotope.SExp.mapAtom Prod.fst

Instances For

def Isotope.SExp.sndAtom {L : Type u_1} {R : Type u_2} :

SExp (L × R) → SExp R

Equations

Isotope.SExp.sndAtom = Isotope.SExp.mapAtom Prod.snd

Instances For

def Isotope.SExp.pswapAtom {L : Type u_1} {R : Type u_2} :

SExp (L × R) → SExp (R × L)

Equations

Isotope.SExp.pswapAtom = Isotope.SExp.mapAtom Prod.swap

Instances For

def Isotope.SExp.zeroAtom {A : Type ua} {A' : Type u_1} :

SExp A → SExp A'

Equations

Isotope.SExp.zeroAtom = Isotope.SExp.substAtom fun (x : A) => ∅

Instances For

@[simp]

theorem Isotope.SExp.zeroAtom_atom {A : Type ua} {A' : Type u_1} (a : A) :

(atom a).zeroAtom = ∅

@[simp]

theorem Isotope.SExp.zeroAtom_par {A : Type ua} {A' : Type u_1} {length : ℕ} (es : Fin length → SExp A) :

(par es).zeroAtom = par fun (i : Fin length) => (es i).zeroAtom

@[simp]

theorem Isotope.SExp.zeroAtom_parL {A A' : Type ua} (es : List (SExp A)) :

(parL es).zeroAtom = parL (zeroAtom <$> es)

@[simp]

theorem Isotope.SExp.zeroAtom_mapAtom {A : Type ua} {A' : Type u_2} {A'' : Type u_1} (f : A → A') (e : SExp A) :

(mapAtom f e).zeroAtom = e.zeroAtom

@[simp]

theorem Isotope.SExp.mapAtom_zeroAtom {A : Type ua} {A' : Type u_2} {A'' : Type u_1} (f : A' → A'') (e : SExp A) :

mapAtom f e.zeroAtom = e.zeroAtom

@[simp]

theorem Isotope.SExp.zeroAtom_zeroAtom {A : Type ua} {A' : Type u_2} {A'' : Type u_1} (e : SExp A) :

e.zeroAtom.zeroAtom = e.zeroAtom

def Isotope.SExp.constAtom {A : Type ua} {C : Type u_1} (c : C) :

SExp A → SExp C

Equations

Isotope.SExp.constAtom c = Isotope.SExp.mapAtom fun (x : A) => c

Instances For

@[simp]

theorem Isotope.SExp.constAtom_atom {A : Type ua} {C : Type u_1} (c : C) (x : A) :

constAtom c (atom x) = atom c

@[simp]

theorem Isotope.SExp.constAtom_par {A : Type ua} {C : Type u_1} (c : C) {length : ℕ} (es : Fin length → SExp A) :

constAtom c (par es) = par fun (i : Fin length) => constAtom c (es i)

@[simp]

theorem Isotope.SExp.constAtom_parL {A C : Type ua} (c : C) (es : List (SExp A)) :

constAtom c (parL es) = parL (constAtom c <$> es)

@[simp]

theorem Isotope.SExp.constAtom_mapAtom {A : Type ua} {A' : Type u_2} {C : Type u_1} (c : C) (f : A → A') (e : SExp A) :

constAtom c (mapAtom f e) = constAtom c e

@[simp]

theorem Isotope.SExp.constAtom_constAtom {A : Type u_1} {C : Type u_2} {C' : Type u_3} (c : C) (c' : C') (e : SExp A) :

constAtom c (constAtom c' e) = constAtom c e

@[simp]

theorem Isotope.SExp.zeroAtom_constAtom {A : Type ua} {A' : Type u_1} {C : Type u_2} (c : C) (e : SExp A) :

(constAtom c e).zeroAtom = e.zeroAtom

@[simp]

theorem Isotope.SExp.constAtom_zeroAtom {A : Type ua} {A' : Type u_2} {C : Type u_1} (c : C) (e : SExp A) :

constAtom c e.zeroAtom = e.zeroAtom

@[reducible, inline]

abbrev Isotope.SExp.eraseAtom {A : Type ua} :

SExp A → SExp Empty

Equations

Isotope.SExp.eraseAtom = Isotope.SExp.zeroAtom

Instances For

@[reducible, inline]

abbrev Isotope.SExp.collapseAtom {A : Type ua} :

SExp A → SExp Unit

Equations

Isotope.SExp.collapseAtom = Isotope.SExp.constAtom ()

Instances For