[Agda] parameters vs indices

Roman effectfully at gmail.com
Tue Jul 11 12:02:24 CEST 2017


Hi.

> Why don't we force people to be Honest instead of just being Good?

No need to force people when you can force indices:
https://hackage.haskell.org/package/Agda-2.5.2/docs/Agda-TypeChecking-Forcing.html

With forcing some things are smaller than without it, see e.g. this
issue: https://github.com/agda/agda/issues/1676


More information about the Agda mailing list