hax
hax copied to clipboard
Array/Slice Patterns are not supported
#[hax_lib::fstar::after("let lemma (a:u8) (b:u8) : Lemma (ensures (f(f([a,b])) == [a,b])) = ()")]
fn f(x: [u8; 2]) -> [u8; 2] {
match x {
[a, b] => [b, a]
}
}
Open this code snippet in the playground
This example results in an error:
error: [HAX0001] (AST import) something is not implemented yet.
Pat:Array
--> src/lib.rs:7:1
|
7 | [a, b] => [b, a]
| ^^^^^^^^^^^^^^
|
info: hax: wrote file /workdir/proofs/fstar/extraction/Playground.fst