---

Step * of Lemma C_TYPE-ext

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeExt

---

Home Index