-ndefinition pseudo_is_comparable ≝
-λmcu:mcu_type.match mcu with
- [ HC05 ⇒ Freescalepseudo_is_comparable
- | HC08 ⇒ Freescalepseudo_is_comparable
- | HCS08 ⇒ Freescalepseudo_is_comparable
- | RS08 ⇒ Freescalepseudo_is_comparable
- | IP2022 ⇒ IP2022pseudo_is_comparable
- ].
+naxiom daemon: False.
+
+ndefinition pseudo_is_comparable: mcu_type → comparable.
+ #mcu;
+ @ (aux_pseudo_type mcu)
+ ##[ napply (match mcu return λmcu. aux_pseudo_type mcu with
+ [ HC05 ⇒ zeroc Freescalepseudo_is_comparable
+ | HC08 ⇒ zeroc Freescalepseudo_is_comparable
+ | HCS08 ⇒ zeroc Freescalepseudo_is_comparable
+ | RS08 ⇒ zeroc Freescalepseudo_is_comparable
+ | IP2022 ⇒ zeroc IP2022pseudo_is_comparable
+ ])
+ | napply (match mcu return λmcu. (aux_pseudo_type mcu → bool) → bool with
+ [ HC05 ⇒ forallc Freescalepseudo_is_comparable
+ | HC08 ⇒ forallc Freescalepseudo_is_comparable
+ | HCS08 ⇒ forallc Freescalepseudo_is_comparable
+ | RS08 ⇒ forallc Freescalepseudo_is_comparable
+ | IP2022 ⇒ forallc IP2022pseudo_is_comparable
+ ])
+ | napply (match mcu return λmcu. aux_pseudo_type mcu → aux_pseudo_type mcu → bool with
+ [ HC05 ⇒ eqc Freescalepseudo_is_comparable
+ | HC08 ⇒ eqc Freescalepseudo_is_comparable
+ | HCS08 ⇒ eqc Freescalepseudo_is_comparable
+ | RS08 ⇒ eqc Freescalepseudo_is_comparable
+ | IP2022 ⇒ eqc IP2022pseudo_is_comparable
+ ])
+ |##*: ncases daemon ]
+nqed.
+