Narya: Field projection from a transported tuple in 3D dimension raises an internal bug
Fixed · medium · Crash
Field projection from a transport in a three-dimensional degeneracy of a record type raises bug E0500 on valid HoTT code. The program is correct, but Narya cannot check it.
Found: ; reported: ; status since: . Reporter: Mike Murunov
Page for this report · Public report · Fix or proposed fix (see status)