From 63cef9b14a8866cf8fbf6e097fc09e36f5bfb321 Mon Sep 17 00:00:00 2001 From: franziskuskiefer Date: Fri, 20 Oct 2023 14:11:12 +0000 Subject: [PATCH] deploy: 1dc669cea553eea55a682c65ade181785f4d02a7 --- posts/hax-v0-1/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/hax-v0-1/index.html b/posts/hax-v0-1/index.html index 615af6e..95607cc 100644 --- a/posts/hax-v0-1/index.html +++ b/posts/hax-v0-1/index.html @@ -68,7 +68,7 @@

This will extract the crate to F*. Similarly, cargo hax into coq will extract the crate to Coq.

For more options use

cargo hax into --help
 

Example

We walk through a sample usage of hax based on an example. -The example can be found in the git repository.

Go to the proofs/fstar/extraction directory and run make. +The example can be found in the git repository.

Go to the proofs/fstar/extraction directory and run make. This will first call

cargo hax into -i '-** +**::process_order' fstar
 

in order to extract the process_order order function to F*. This demonstrates one particularly useful feature in hax, which allows extracting