Translate the JSON values generated by the parser to the corresponding fixtype JSON values.
Theorem:
(defthm return-type-of-parsed-to-value.erp (b* (((mv ?erp ?value) (parsed-to-value x))) (booleanp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-value.value (b* (((mv ?erp ?value) (parsed-to-value x))) (valuep value)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-value-list.erp (b* (((mv ?erp ?values) (parsed-to-value-list x))) (booleanp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-value-list.values (b* (((mv ?erp ?values) (parsed-to-value-list x))) (value-listp values)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-member.erp (b* (((mv ?erp ?member) (parsed-to-member x))) (booleanp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-member.member (b* (((mv ?erp ?member) (parsed-to-member x))) (memberp member)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-member-list.erp (b* (((mv ?erp ?members) (parsed-to-member-list x))) (booleanp erp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parsed-to-member-list.members (b* (((mv ?erp ?members) (parsed-to-member-list x))) (member-listp members)) :rule-classes :rewrite)