Skip to content

Conversation

gebner
Copy link
Contributor

@gebner gebner commented Oct 2, 2025

A picture is worth a thousand words:

-let (update_env_polymonadic_bind :
-  FStarC_TypeChecker_Env.env ->
-    FStarC_Ident.lident ->
-      FStarC_Ident.lident ->
-        FStarC_Ident.lident ->
-          FStarC_Syntax_Syntax.tscheme ->
-            FStarC_Syntax_Syntax.indexed_effect_combinator_kind ->
-              FStarC_TypeChecker_Env.env)
-  =
-  fun env ->
-    fun m ->
-      fun n ->
-        fun p ->
-          fun ty ->
-            fun k ->
-              FStarC_TypeChecker_Env.add_polymonadic_bind env m n p
-                (fun env1 ->
-                   fun c1 ->
-                     fun bv_opt ->
-                       fun c2 ->
-                         fun flags ->
-                           fun r ->
-                             mk_indexed_bind env1 m n p ty k c1 bv_opt c2
-                               flags r Prims.int_zero false)
+let update_env_polymonadic_bind (env : FStarC_TypeChecker_Env.env)
+  (m : FStarC_Ident.lident) (n : FStarC_Ident.lident)
+  (p : FStarC_Ident.lident) (ty : FStarC_Syntax_Syntax.tscheme)
+  (k : FStarC_Syntax_Syntax.indexed_effect_combinator_kind) :
+  FStarC_TypeChecker_Env.env=
+  FStarC_TypeChecker_Env.add_polymonadic_bind env m n p
+    (fun env1 c1 bv_opt c2 flags r ->
+       mk_indexed_bind env1 m n p ty k c1 bv_opt c2 flags r Prims.int_zero
+         false)

The wild thing is that this causes a 10% reduction in binary code size:

  • fstarc.exe: 69M → 63M
  • pulse.cmxs: 12M → 11M

@gebner gebner force-pushed the gebner_pretty_mllet branch from 92e7d28 to 37e723c Compare October 3, 2025 00:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant