Qcert.NNRC.Typing.TNNRC
Typing rules for NNRC
Section typ.
Context {m:basic_model}.
Definition nnrc_ext_type (env:tbindings) (n:nnrc) (t:rtype) : Prop :=
nnrc_type env (nnrc_ext_to_nnrc n) t.
End typ.
Context {m:basic_model}.
Definition nnrc_ext_type (env:tbindings) (n:nnrc) (t:rtype) : Prop :=
nnrc_type env (nnrc_ext_to_nnrc n) t.
End typ.
Main lemma for the type correctness of NNNRC
Theorem typed_nnrc_ext_yields_typed_data {m:basic_model} {τ} (env:bindings) (tenv:tbindings) (e:nnrc) :
bindings_type env tenv →
nnrc_ext_type tenv e τ →
(∃ x, (@nnrc_ext_eval _ brand_relation_brands env e) = Some x ∧ (data_type x τ)).
Global Instance nnrc_ext_type_lookup_equiv_prop {m:basic_model} :
Proper (lookup_equiv ==> eq ==> eq ==> iff) nnrc_ext_type.
End TNNRC.