Qcert.NRA.Typing.TNRAExt
Typing for NRA
Context {m:basic_model}.
Definition nraext_type Op A B := nra_type (nra_of_nraext Op) A B.
Notation "Op ▷ A >=> B" := (nraext_type Op A B) (at level 70).
Main typing soundness theorem for the Extended NRA
Theorem typed_nraext_yields_typed_data {τin τout} (d:data) (op:nraext):
(d ▹ τin) → (op ▷ τin >=> τout) →
(∃ x, (brand_relation_brands ⊢ op @ₓ d = Some x ∧ (x ▹ τout))).
Corrolaries of the main type soudness theorem
Definition typed_nraext_total {τin τout} (op:nraext) (d:data):
(d ▹ τin) → (op ▷ τin >=> τout) →
{ x:data | x ▹ τout }.
Definition tnraext_eval {τin τout} (op:nraext) (d:data):
(d ▹ τin) → (op ▷ τin >=> τout) → data.
End TNRAExt.
Notation "Op ▷ A >=> B" := (nraext_type Op A B) (at level 70) : nraext_scope.
Notation "Op @▷ d" := (tnraext_eval Op d) (at level 70) : nraext_scope.