Right now, a value has a constructor for Error terms (V_Error), which is bad naming. Instead, we should remove the constructor and introduce a new type
Inductive result : Term -> Prop :=
| R_value : forall t, value t -> result t
| R_error : forall ty, result (Error ty)
This will simplify RG which should only contain values, not errors.
Right now, a
value
has a constructor for Error terms (V_Error
), which is bad naming. Instead, we should remove the constructor and introduce a new typeThis will simplify
RG
which should only contain values, not errors.