Lucas Franceschino

Hi, This PR adds reflection for quotations, allowing for static or dynamic quotations and anti-quotations to be inspected and constructed from the reflection API. This feature is particularly useful for...

QuasiQuotes for F*

2

Hi, This (draft) PR adds some support for quasi-quotes in F*, with a syntax similar to [Haskell's quasi-quotes](https://wiki.haskell.org/Quasiquotation). It's quite experimental for now, and I wanted to have some feedback...

Expose term parsing in tactics via `string_to_term`

6

Hello, Here is a PR that brings term parsing to tactics, via a primitive `string_to_term`, that takes a string and an environement. I hope to write a sort of REPL...

Hi, This PR makes the following record expression and type declaration valid: ```fstar type foo = { ( ^ ): int } let _: foo = { ( ^ )...

Improvements over let operators

1

Hi, Following the conversation in #1868, this PR improves the implementations of let operators in the following ways: - simplify the parser by letting `let` and `and` be treated as...

Parser: accept `f {field = ...}` (no need for `f ({field = ...})` anymore)

2

Hi, This PR changes a bit the parser rules related to function application so that the expression `f {foo = 123}` is now allowed. Previously, `f {foo = 123}` was...

Hi, This PR adds a rule to the parser and adds a node `PatVQuote` to the surface AST so that ``​`%foo`` is now a legal pattern. `PatVQuote` nodes are desugared...

Hi, I was using the reflection API in a total context and found some `inspect_*` primitive were lacking refinements, forcing me to add `admit`s about termination of some of my...

Add support for data constructors attributes

2

Hi, This PR adds support for decorating data constructors (and records) with attributes, as @TWal was suggesting a few days ago on Slack. The syntax follows the one for binders,...

`term_to_string` being total implies ⊥

2

Hi, `term_to_string` is a `Tot` computation despite being impure because sensitive to the options `hide_uvar_nums`, `print_bound_var_types`, `print_effect_args`, `print_implicits`, `print_real_names`, `print_universes` and `ugly`. Thus one can derive `⊥` easily by observing...