hax icon indicating copy to clipboard operation
hax copied to clipboard

Array/Slice Patterns are not supported

Open karthikbhargavan opened this issue 1 year ago • 0 comments

#[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

karthikbhargavan avatar Jul 25 '24 15:07 karthikbhargavan