You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I'm trying to resurrect the student's attempt at a normalization proof in F* but the positivity check gets in the way. I think the positivity check should be a non-fatal error, in the same class as being unable to discharge a proof obligation, but that's currently not the case. Alternatively I would like a flag to turn off the positivity check completely, so that I can fix the other potential errors that have nothing to do with positivity.
This is implemented in the positivity_check function in tc.fs, but I'm not sure with what to replace the raise to make it non-fatal.
The text was updated successfully, but these errors were encountered:
catalin-hritcu
changed the title
Make positivity check non-fatal
Make positivity check non-fatal (or disablable)
Jul 13, 2015
I'm trying to resurrect the student's attempt at a normalization proof in F* but the positivity check gets in the way. I think the positivity check should be a non-fatal error, in the same class as being unable to discharge a proof obligation, but that's currently not the case. Alternatively I would like a flag to turn off the positivity check completely, so that I can fix the other potential errors that have nothing to do with positivity.
This is implemented in the
positivity_check
function intc.fs
, but I'm not sure with what to replace theraise
to make it non-fatal.The text was updated successfully, but these errors were encountered: