An illegal record field is not 'redundant'

FStarLang / FStar

A Proof-oriented Programming Language

https://fstar-lang.org

Apache License 2.0

2.7k stars 234 forks source link

Open briangmilnes opened 1 month ago

briangmilnes commented 1 month ago

Error 118 at src/fstar/fst/FStar.Flog.fst(23,5-23,11):
- Field 'startS' is redundant for type FStar.Flog.flog_config

Should say something clearer, such as no such field startS in type.