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 bumped into this validating Sheera's DFS, so I wrote some small test files.
Error 98 at src/LetLemmaInFSTI.fst(1,7-1,21):
Some interface elements were not implemented by module LetLemmaInFSTI:
val four_gt_three
let three_gt_two
If you put a val+let lemma in an fsti and don't provide the val the following let is also
reported as not implemented which is incorrect in that the fsti provides the lemma.
FSTI:
/// This tests putting a let lemma in an fsti and not in the fst.
module LetLemmaInFSTI
val four_gt_three () : Lemma (4 > 3)
let three_gt_two () : Lemma (3 > 2) = ()
FST:
module LetLemmaInFSTI
/// No three_gt_two.
The text was updated successfully, but these errors were encountered:
I bumped into this validating Sheera's DFS, so I wrote some small test files.
val four_gt_three
let three_gt_two
If you put a val+let lemma in an fsti and don't provide the val the following let is also
reported as not implemented which is incorrect in that the fsti provides the lemma.
FSTI:
/// This tests putting a let lemma in an fsti and not in the fst.
module LetLemmaInFSTI
val four_gt_three () : Lemma (4 > 3)
let three_gt_two () : Lemma (3 > 2) = ()
FST:
module LetLemmaInFSTI
/// No three_gt_two.
The text was updated successfully, but these errors were encountered: