---

Step * of Lemma C_TYPEco-ext

C_TYPEco() ≡ lbl:Atom × if lbl =a "Void" then Unit
                        if lbl =a "Int" then Unit
                        if lbl =a "Struct" then (Atom × C_TYPEco()) List
                        if lbl =a "Array" then length:ℕ × C_TYPEco()
                        if lbl =a "Pointer" then C_TYPEco()
                        else Void
                        fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
C\_TYPEco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Void"  then  Unit
                                                if  lbl  =a  "Int"  then  Unit
                                                if  lbl  =a  "Struct"  then  (Atom  \mtimes{}  C\_TYPEco())  List
                                                if  lbl  =a  "Array"  then  length:\mBbbN{}  \mtimes{}  C\_TYPEco()
                                                if  lbl  =a  "Pointer"  then  C\_TYPEco()
                                                else  Void
                                                fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index