Explicit (hax-engine.Hax_engine.Ast

val ty_unit : AST.ty

val expr_unit : span:Ast.span -> Hax_engine__Ast.Make(F).expr

val expr_tuple : span:Ast.span -> AST.expr Prelude.list -> AST.expr

val pat_PBinding : 
  typ:Hax_engine__Ast.Make(F).ty ->
  span:Ast.span ->
  mut:F.mutable_variable Ast.mutability ->
  mode:Hax_engine__Ast.Make(F).binding_mode ->
  var:Ast.local_ident ->
  subpat:(Hax_engine__Ast.Make(F).pat * F.as_pattern) Prelude.option ->
  Hax_engine__Ast.Make(F).pat

val arm : 
  span:Span.t ->
  AST.pat ->
  ?guard:AST.guard Prelude.option ->
  AST.expr ->
  AST.arm

val pat_Constructor_CF : 
  span:Ast.span ->
  typ:AST.ty ->
  [ `Break | `Continue ] ->
  AST.pat ->
  AST.pat

val call_Constructor' : 
  Ast.global_ident ->
  Prelude.bool ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val call_Constructor : 
  Concrete_ident.name ->
  Prelude.bool ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val expr'_Constructor_CF : 
  span:Ast.span ->
  break_type:AST.ty ->
  ?continue_type:AST.ty ->
  [ `Break | `Continue ] ->
  AST.expr ->
  AST.expr

val expr_Constructor_CF : 
  span:Ast.span ->
  break_type:AST.ty Prelude.option ->
  return_type:AST.ty Prelude.option ->
  acc:AST.expr ->
  ?e:AST.expr ->
  [ `Break | `Continue | `Return ] ->
  AST.expr

We use the following encoding of return, break and continue in the `ControlFlow` enum: Return e -> Break (Break e) Break e -> Break ((Continue(e, acc))) Continue -> Continue(acc)

In case there is no return we simplify to: Break e -> (Break (e, acc)) Continue -> (continue (acc))