Théophile Wallez

Test.fsti: ```fstar module Test ``` Test.fst: ```fstar module Test let x:int = 0 let y:int = Test.x ``` ``` $ fstar.exe Test.fst * Error 117: - You may have a...

Normalizer has weird behavior with one-element lists (again)

1

Following the resolution of #3353, I can now use my `squash (norm ...)` construct in my proofs, however, I need to prove it first! I am again noticing a weird...