FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Published 20 hours ago • verified publisher icon FStarLang

Quantifiers uncurrying in resugar is buggy

Open aseemr opened this issue 3 years ago • 0 comments

A formula like forall x1. forall. x2. exists x3. phi gets resugared to, and hence pretty printed as, forall x1 x2 x3. phi. The bug is in the uncurry function in FStar.Syntax.Reguar.fs.

aseemr avatar Sep 24 '21 09:09 aseemr