[Paper Artifact] Equational Reasoning for Probabilistic Programming

_CoqProject

@@ -136,3 +136,11 @@ theories/showcase/pnt.v
 
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.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/lang_syntax_table_game.v
+theories/lang_syntax_noisy.v

coq-mathcomp-analysis.opam

@@ -19,6 +19,7 @@ depends: [
   "coq-mathcomp-solvable"
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
+  "coq-mathcomp-algebra-tactics" { (>= "1.2.4") }
 ]
 
 tags: [

coq-mathcomp-classical.opam

@@ -20,8 +20,8 @@ depends: [
   "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
-  "coq-mathcomp-finmap" { (>= "2.1.0") }
-  "coq-hierarchy-builder" { (>= "1.8.0") }
+  "coq-mathcomp-finmap" { (>= "2.2.0") }
+  "coq-hierarchy-builder" { (>= "1.8.1") }
 ]
 
 tags: [

theories/Make

@@ -97,3 +97,11 @@ pi_irrational.v
 gauss_integral.v
 all_analysis.v
 showcase/summability.v
+prob_lang.v
+prob_lang_wip.v
+lang_syntax_util.v
+lang_syntax_toy.v
+lang_syntax.v
+lang_syntax_examples.v
+lang_syntax_table_game.v
+lang_syntax_noisy.v