Questions tagged [sized-types]

Sized types are types annotated with size information, which is used by the termination checker for complex non-structural recursion termination check.

Filter by
Sorted by
Tagged with
8 votes
1 answer
143 views

Is it possible to define `fib` coinductive stream w/o sized types?

In Agda with --guardedness, we can define productive definitions using copatterns like the following ...
ice1000's user avatar
  • 5,974