nikswamy

I tried this out today and it doesn't seem to work for my scenario which involves external types. Consider: ``` module Test module B = LowStar.Buffer assume val _MY_EXTERNAL_TYPE :...

hi @Alan-Jowett When building EverParse generated code with the Visual C/C++ compiler, we use the following settings /W4 /WX /wd4127 /wd4204 /wd4100 /wd4201 Where, we suppress: * error C4100: unreferenced...

Not much progress on this since the Cambridge all-hands summit, I'm afraid. I've mostly been working on many F\* features in support of Kremlin/Record layer, notably more normalization. Also, I've...

The result type is an `optResult`. I would have expected the implementation to do a dynamic test on the length of the substring and return the `Error` case of optResult...

How about we just detect the lower-case filename in 3d and immediately print an error requesting an upper-case filename? Part of the annoyance with this issue is that the failure...

No. This would allow bad things like `match e with | A -> 0 | _ -> 1` to unify with `match e with | _ -> 0 | _...

Rejecting impredicativity is certainly an option we should keep on the table.

Erased types were designed for erasure. I didn't have proof irrelevance in mind at all. I don't think we'd want something like reveal in Prop.

But if you chose that representation how would you implement map_squash?

Renaming the issue. Who wants to take on writing some of these examples? @kyoDralliam @s-zanella @catalin-hritcu ?