Skip to content

Commit

Permalink
deploy: 1dc669c
Browse files Browse the repository at this point in the history
  • Loading branch information
franziskuskiefer committed Oct 20, 2023
1 parent 00bc620 commit 63cef9b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion posts/hax-v0-1/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@
</span></span></code></pre></div><p>This will extract the crate to F*.
Similarly, <code>cargo hax into coq</code> will extract the crate to Coq.</p><p>For more options use</p><div class=highlight><pre tabindex=0 class=chroma><code class=language-bash data-lang=bash><span class=line><span class=cl>cargo hax into --help
</span></span></code></pre></div><h1 id=example>Example<a hidden class=anchor aria-hidden=true href=#example>#</a></h1><p>We walk through a sample usage of hax based on an example.
The example can be found in the <a href=https://github.com/hacspec/hax/tree/main/examples/lob>git repository</a>.</p><p>Go to the <code>proofs/fstar/extraction</code> directory and run <code>make</code>.
The example can be found in the <a href=https://github.com/hacspec/hax/tree/main/examples/limited-order-book>git repository</a>.</p><p>Go to the <code>proofs/fstar/extraction</code> directory and run <code>make</code>.
This will first call</p><pre tabindex=0><code>cargo hax into -i &#39;-** +**::process_order&#39; fstar
</code></pre><p>in order to extract the <code>process_order</code> order function to F*.
This demonstrates one particularly useful feature in hax, which allows extracting
Expand Down

0 comments on commit 63cef9b

Please sign in to comment.