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) = ()
I bumped into this validating Sheera's DFS, so I wrote some small test files.
FST: module LetLemmaInFSTI /// No three_gt_two.