FStar icon indicating copy to clipboard operation
FStar copied to clipboard

F* can't find one enum constructor after it found an isomorphic one

Open briangmilnes opened this issue 1 year ago • 4 comments

/// BUG F* can't find Three either as WrapOCaml.Three or Three !! /// This works above for enum One which is only trivially different. /// It works in language server but not with either a recent /// dev release or an opam development release. /// The OCaml is not required for this bug. /// F* 2024.08.14~dev /// platform=Linux_x86_64 /// compiler=OCaml 4.14.2 /// date=2024-09-02 15:23:16 -0700 /// commit=445f713ad8b276864ba7e205e028813e19324b66

Compile line from Forge make: /// /home/milnes/.opam/default/bin/fstar.exe --warn_error "-321-333-331" --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes --print_implicits --cache_checked_modules --cache_dir _build/fstar/fst/checked --include src --include src/fstar/ --include src/fstar/fst/ --include /home/milnes/.opam/default/lib/fstar src/fstar/fst/Main.fst

See Main.fst line 132. Main.txt WrapOCaml.txt

The compilation in Forge is not needed to test this.

briangmilnes avatar Sep 16 '24 17:09 briangmilnes