Axiom norm : Ty -> Ty.
Axiom norm_normalise : forall ty, normalise ty (norm ty).
Axiom map_norm : list (string * Ty) -> list (string * Ty).
Axiom map_norm_map_normalise : forall Ts, map_normalise Ts (map_norm Ts).
map_norm and map_norm_map_normalise can actually be implemented in terms of norm and norm_normalise.
When refactoring proofs to use this instead of normalise Tb Tbn assumptions, things will break. For example tactics that construct typing derivations. Perhaps it is better to also update has_type definition to use these functions instead.
map_norm
andmap_norm_map_normalise
can actually be implemented in terms ofnorm
andnorm_normalise
.When refactoring proofs to use this instead of
normalise Tb Tbn
assumptions, things will break. For example tactics that construct typing derivations. Perhaps it is better to also updatehas_type
definition to use these functions instead.