Expect (hax-engine.Fstar_backend.Attrs.U.Expect)

val mut_borrow : AST.expr -> AST.expr Hax_engine.Prelude.option

val borrow : AST.expr -> AST.expr Hax_engine.Prelude.option

val block : AST.expr -> AST.expr Hax_engine.Prelude.option

val deref : AST.expr -> AST.expr Hax_engine.Prelude.option

val closure : 
  AST.expr ->
  (AST.pat Hax_engine.Prelude.list * AST.expr) Hax_engine.Prelude.option

val app : 
  AST.expr ->
  (AST.expr
   * AST.expr Hax_engine.Prelude.list
   * AST.generic_value Hax_engine.Prelude.list
   * AST.impl_expr Hax_engine.Prelude.option
   * AST.impl_expr Hax_engine.Prelude.list)
    Hax_engine.Prelude.option

val pbinding_simple : 
  AST.pat ->
  (Hax_engine.Ast.local_ident * AST.ty) Hax_engine.Prelude.option

val concrete_app1 : 
  Hax_engine.Concrete_ident.name ->
  AST.expr ->
  AST.expr Hax_engine.Prelude.option

val deref_mut_app : AST.expr -> AST.expr Hax_engine.Prelude.option

val local_var : AST.expr -> AST.expr Hax_engine.Prelude.option

val arrow : 
  AST.ty ->
  (AST.ty Hax_engine.Prelude.list * AST.ty) Hax_engine.Prelude.option

val mut_ref : AST.ty -> AST.ty Hax_engine.Prelude.option

val concrete_app' : 
  AST.expr' ->
  Hax_engine.Ast.concrete_ident Hax_engine.Prelude.option