TBT: Bug in size preservation regarding local definitions #7271
Labels
false
Proof of the empty type which checks without known-unsafe flags (e.g. without --type-in-type)
maculata
Issue with a so far unreleased feature (not in changelog)
type: bug
Issues and pull requests about actual bugs
type-based-termination
Concerning `--type-based-termination`
Milestone
TBT accepts a non-productive definition, which we can exploit to make the Agda loop:
ATTN: @knisht
The text was updated successfully, but these errors were encountered: