add our "type size benchmark": the type of wpF (the function wp is the fixed point of)

iris.v

@@ -26,6 +26,21 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
   Instance Props_BI : ComplBI Props | 0 := _.
   Instance Props_Later : Later Props | 0 := _.
 
+  (* Benchmark: How large is thid type? *)
+  Section Benchmark.
+    Local Open Scope mask_scope.
+    Local Open Scope pcm_scope.
+    Local Open Scope bi_scope.
+    Local Open Scope lang_scope.
+
+    Local Instance expr_type : Setoid expr := discreteType.
+    Local Instance expr_metr : metric expr := discreteMetric.
+    Local Instance expr_cmetr : cmetric expr := discreteCMetric.
+
+    Set Printing All.
+    Check ((expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props).
+  End Benchmark.
+
   (** And now we're ready to build the IRIS-specific connectives! *)
 
   Section Necessitation.
@@ -388,6 +403,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   End Erasure.
 
+
   Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
 
   Section ViewShifts.