Skip to content

Commit 75ce06e

Browse files
committed
This month in hax november description.
1 parent af814cf commit 75ce06e

File tree

2 files changed

+6
-1
lines changed

2 files changed

+6
-1
lines changed

docs/blog/posts/this-month-in-hax/2025-11.md

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,11 @@ date: 2025-12-01
77

88
In November, we successfully merged **16 pull requests**!
99

10-
<DESCRIPTION>
10+
The frontend continues getting improvements thanks to [@Nadrieril](https://github.com/Nadrieril).
11+
So does the lean backend, with support for default methods and lib improvements including renaming the `Result` monad to `RustM`.
12+
The lib has been the focus as we now have started incorporating the new core models written in Rust.
13+
A first batch of changes already happened in November and are automatically extracted to the F* library (manually for lean).
14+
We continue the development of these models which will hopefully cover all we already have in the F* lib as manual F* models.
1115

1216
### Full list of PRs
1317
* \#1778: [Change impl_u64__rotate_right second parameter type to u32](https://github.com/cryspen/hax/pull/1778)

engine/lib/import_thir.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1189,6 +1189,7 @@ end) : EXPR = struct
11891189
(* fun _ -> Ok Bool *)
11901190

11911191
and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
1192+
Logs.info (fun m -> m "span: %s" ([%show: Thir.span] span));
11921193
let goal = c_trait_ref span ie.trait.value in
11931194
let impl = { kind = c_impl_expr_atom span ie.impl goal; goal } in
11941195
match ie.impl with

0 commit comments

Comments
 (0)