Type of a literal.
In Syntheto, each literal has an obvious primitive type.
Function:
(defun literal-type (lit) (declare (xargs :guard (literalp lit))) (let ((__function__ 'literal-type)) (declare (ignorable __function__)) (literal-case lit :boolean (type-boolean) :character (type-character) :string (type-string) :integer (type-integer))))
Theorem:
(defthm typep-of-literal-type (b* ((type (literal-type lit))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm literal-type-of-literal-fix-lit (equal (literal-type (literal-fix lit)) (literal-type lit)))
Theorem:
(defthm literal-type-literal-equiv-congruence-on-lit (implies (literal-equiv lit lit-equiv) (equal (literal-type lit) (literal-type lit-equiv))) :rule-classes :congruence)