(* *)
(**************************************************************************)
-include "ground_2/notation/relations/ringeq_3.ma".
+include "ground/notation/relations/ringeq_3.ma".
include "apps_2/notation/models/at_3.ma".
+include "apps_2/notation/models/oplus_4.ma".
include "apps_2/notation/models/wbrackets_4.ma".
include "static_2/syntax/term.ma".
(* MODEL ********************************************************************)
record model: Type[1] ≝ {
- dd: Type[0]; (* denotations domain *)
- sq: relation2 dd dd; (* structural equivalence *)
- sv: nat → dd; (* sort evaluation *)
- ap: dd → dd → dd; (* application *)
- ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *)
+(* Note: denotations domain *)
+ dd: Type[0];
+(* Note: structural equivalence *)
+ sq: relation2 dd dd;
+(* Note: sort evaluation *)
+ sv: nat → dd;
+(* Note: conjunction *)
+ co: bool → dd → dd → dd;
+(* Note: application *)
+ ap: dd → dd → dd;
+(* Note: term interperpretation *)
+ ti: (nat → dd) → (nat → dd) → term → dd
}.
interpretation "structural equivalence (model)"
interpretation "application (model)"
'At M d1 d2 = (ap M d1 d2).
+interpretation "conjunction (model)"
+ 'OPlus M p d1 d2 = (co M p d1 d2).
+
interpretation "term interpretation (model)"
'WBrackets M gv lv T = (ti M gv lv T).