syntax and denotational semantics

Co-authored-by: Reynald Affeldt <[email protected]>

_CoqProject

@@ -46,6 +46,10 @@ theories/charge.v
 theories/kernel.v
 theories/prob_lang.v
 theories/prob_lang_wip.v
+theories/lang_syntax_util.v
+theories/lang_syntax_toy.v
+theories/lang_syntax.v
+theories/lang_syntax_examples.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

coq-mathcomp-analysis.opam

@@ -22,6 +22,7 @@ depends: [
   "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.18~") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
+  "coq-mathcomp-algebra-tactics" { (>= "1.1.1") }
 ]
 
 tags: [

theories/Make

@@ -37,6 +37,10 @@ charge.v
 kernel.v
 prob_lang.v
 prob_lang_wip.v
+lang_syntax_util.v
+lang_syntax_toy.v
+lang_syntax.v
+lang_syntax_examples.v
 altreals/xfinmap.v
 altreals/discrete.v
 altreals/realseq.v

theories/kernel.v

@@ -74,7 +74,7 @@ HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d')
 HB.structure Definition Kernel d d'
     (X : measurableType d) (Y : measurableType d') (R : realType) :=
   { k & isKernel _ _ X Y R k }.
-Notation "R .-ker X ~> Y" := (kernel X Y R).
+Notation "R .-ker X ~> Y" := (kernel X%type Y R).
 
 Arguments measurable_kernel {_ _ _ _ _} _.
 
@@ -177,7 +177,7 @@ HB.structure Definition SFiniteKernel d d'
     (X : measurableType d) (Y : measurableType d') (R : realType) :=
   { k of @Kernel _ _ _ _ R k &
          Kernel_isSFinite_subdef _ _ X Y R k }.
-Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X Y R).
+Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X%type Y R).
 Arguments sfinite_kernel_subdef {_ _ _ _ _} _.
 
 Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d')
@@ -200,7 +200,7 @@ HB.structure Definition FiniteKernel d d'
     (X : measurableType d) (Y : measurableType d') (R : realType) :=
   { k of @SFiniteKernel _ _ _ _ _ k &
          SFiniteKernel_isFinite _ _ X Y R k }.
-Notation "R .-fker X ~> Y" := (finite_kernel X Y R).
+Notation "R .-fker X ~> Y" := (finite_kernel X%type Y R).
 Arguments measure_uub {_ _ _ _ _} _.
 
 HB.factory Record Kernel_isFinite d d'