Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Macro inlining: doesn't work in module located in non-root file

Waiting on #145

Inlining of a macro call comming from another macro expansion

Waiting on #145

Attributes: introduce them in engine's AST

Re-opening this issue, PR #106 only added support in the frontend exporter, not in the engine.

How to distribute proofs with Rust code?

@ROMemories, I missed your comment here, sorry. We previously had hand-edited F* extractions, at some point. Thus, we needed to keep the generated code. But now, we have many more...

Make coq backend parse all examples

@cmester0, what do you think about this one? are we there yet, shall we close this?

Make coq backend parse all examples

This is stale, let's close.

Document the generic printer and how to write a backend

Let's close, #533 is going to replace the generic printer, hopefully with some documentation.

F*: pattern matching is disallowed on `usize`s, `isize`s (+`u128`/`i128`)

> The issue is that we do not know the size of `usize` on the target platform. So, it is better to cast the `usize` into `u8`or `u16` or whatever...

Add match guard to AST

Hi Lasse, thanks for the PR, supporting guards on arms would indeed be great. Both let guards on arms and let chains on `if` and arms are nightly: I wonder...

Add logging to Generic Printer

Do you still want to work on that @jschneider-bensch?