nikswamy

Results 77 comments of nikswamy

`unfold` don't work as expected in binder attributes

Thanks @TWal . This is an interesting example. I don't think the attribute annotations were designed to be programmable in this sense. The attributes are interpreted literally, and not up...

I made .NET F# package for F*. Shall I merge?

@mateuszbujalski , any thoughts about this? You have done some similar work

Meta-issue: Steel inference, framing, and selectors

Trying to use Steel.FramingEffect in the branch steel_framing ecafe7d43646b05403307d0e779dff6ce72a4781 1. Fails with Tot and SteelT not composable ``` let test (p:slprop) : SteelT unit p (fun _ -> p) =...

Subtyping and unification in the tactics engine requires re-checking solutions (Was: The unification in tactics is unsound)

Thanks for all the work on this @857b! This is really appreciated. As you can see, @aseemr and I have been trying to find an acceptable fix. For some context,...

Subtyping and unification in the tactics engine requires re-checking solutions (Was: The unification in tactics is unsound)

We have merged PR #2639, with comments there stating that although our current patches are designed to prevent this kind of exploit, we are still working on a more definitive...

Dependent pattern match on pairs doesn't work; need to use nested pattern-match instead

With @aseemr today, we were revisiting this (also in the context of PR #2473) It turns out the problem appears because F* has not yet fully inferred the type of...

Enable subtyping in ctrl_rewrite (and hence, l_to_r)

Overall, this looks pretty good. However, it would be great to have some test cases for l_to_r that exploit the new behavior. It could be something like the examples from...

The type of `/\` and related connectives does not reflect their left-to-right bias (Was: The typechecking of `l_and` as a lazy operator is unsound)

The fixes in PR #2639 prevent the final exploit in these examples that allow extracting a proof of False. As such, I'm removing the unsoundness label. However, I agree that...

`term_to_string` being total implies ⊥

We discussed this at a recent F* meeting. The simplest and cleanest fix seems to be option 1. Do you have a scenario where you specifically rely on the totality...

Should `--dep` really emit `.krml` targets for files explicitly excluded by `--extract` ?

Thanks for warning about this possible breakage, Jonathan @msprotz Just to make sure we're all on the same page, the current behavior of --dep includes this: ``` let all_ml_files =...