Meta F* entry points

(Page under construction)

https://arxiv.org/abs/1803.06547

(tau represents a metaprogram throughout this document)

Proving

Fine-grained: assert phi by tau (and with_tactic)

For a whole VC: let x : C by tau = e and e <: t by tau

Generating terms

Fine grained: synth tau and _ by tau

Generating definitions: %splice

Solving implicit arguments

Meta-implicits: (#[tau] x : t) -> ..

Typeclasses: #a:Type -> {|num a|} -> ...

Postprocessing

postprocess_with attribute

postprocess_for_extraction_with attribute