Skip to content

Commit

Permalink
chore: refresh snapshots
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Nov 28, 2024
1 parent 458954f commit 14e4ede
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 0 deletions.
3 changes: 3 additions & 0 deletions test-harness/src/snapshots/toolchain__literals into-coq.snap
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,9 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s
let _ : t_usize := impl__Int__to_usize (x) in
impl__Int__to_u8 (f_add (x) (f_mul (x) (x))).

Definition null : ascii :=
"\000"%char.

Definition numeric (_ : unit) : unit :=
let _ : t_usize := 123 in
let _ : t_isize := -42 in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,8 @@ let math_integers (x: Hax_lib.Int.t_Int)
let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)

let null: char = '\0'

let numeric (_: Prims.unit) : Prims.unit =
let (_: usize):usize = sz 123 in
let (_: isize):isize = isz (-42) in
Expand Down

0 comments on commit 14e4ede

Please sign in to comment.