FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Published 20 hours ago • verified publisher icon FStarLang

Expose the `unascribe` normalisation step

Open 857b opened this issue 3 years ago • 1 comments

This PR exposes the unascribe normalisation step. It can be useful to get more readable terms and it also seems to speed up some normalisations. I have just exposed the existing Unascribe step, using ZetaFull as a model.

857b avatar Jul 28 '22 09:07 857b

CLA assistant check
All CLA requirements met.

ghost avatar Jul 28 '22 09:07 ghost

Thanks @857b!

aseemr avatar Sep 01 '22 05:09 aseemr