autoclrs/common/Predicates.fst: filename does not match module declaration

[zachary-kent]

Bug

autoclrs/common/Predicates.fst declares module CLRS.Common.Predicates, but the filename lacks the CLRS.Common. prefix that all sibling files use:

autoclrs/common/CLRS.Common.Complexity.fst
autoclrs/common/CLRS.Common.CountOnes.fst
autoclrs/common/CLRS.Common.ListLemmas.fst
autoclrs/common/CLRS.Common.SortSpec.fst
autoclrs/common/Predicates.fst       ← should be CLRS.Common.Predicates.fst
autoclrs/common/Predicates.fsti      ← should be CLRS.Common.Predicates.fsti

This causes F* Error 141 when verifying the file:

* Error 141 at Predicates.fst(1,0-1,29):
  - Interactive mode only supports a single module at the top-level. Expected module Predicates

Fix

Rename the files:

• Predicates.fst → CLRS.Common.Predicates.fst
• Predicates.fsti → CLRS.Common.Predicates.fsti

Reproduction

fstar.exe --lax --admit_smt_queries true --include autoclrs/common autoclrs/common/Predicates.fst