Custom attributes

This page lists the known custom attributes available to F* programs.

Reminder: attributes are arbitrary F* terms, attached to top-level declarations, of the form [@ t₁ t₂ … tₙ]. Example:

[@ "c_inline" ]
let f x = FStar.UInt32.( x *^ x )

Attributes can be attached to any top-level signature elements.

Here's the list of known attributes:

• [@ "c_inline" ] (function): generate a C inline qualifier when extracting via KreMLin
• [@ "substitute" ] (function, deprecated): ask KreMLin to inline the function body at every call-site, possibly introducing intermediary let-bindings for effective arguments that cannot be syntactically determined to be values. Deprecated; use inline_for_extraction instead.
• [@ "inline_let"] (local let): substitute the definition. Often used to guarantee erasure of non-Low* code.
• [@ "opaque_to_smt" ] (function): make the function transparent to F* and reducible by the F* normalizer, but force the SMT-solver to reason equationally about it
• [@ PpxDerivingShow ] (type): the given type, once extracted to OCaml, will be post-fixed by [@@ deriving show ], meaning that a pretty-printer for it will be automatically generated
• [@ (PpxDerivingShowConstant "None") ] (type): the given type, once extracted to OCaml, will be post-fixed by [@printer fun fmt _ -> Format.pp_print_string fmt "None"] followed by [@@ deriving show]; this is useful for generating constant printers

The PpxDerivingShow* attributes, when applied to a type foo, automatically give rise to functions show_foo in the OCaml scope, unless the type is named t, in which case the function is show. To leverage these debugging printers in your F* program, do:

myprogram.fst

module MyProgram

[@ PpxDerivingShow ]
type t = | A | B

noextract
assume val show: t -> string

let debug (x: t) =
  FStar.IO.print_string "debugging!\n";
  FStar.IO.print_string (MyPrinters.show x)