[Agda] complex indices

Brandon Moore brandon_m_moore at yahoo.com
Wed Feb 22 22:18:49 CET 2012


> Yes but I think the return type in my example was Set.
> Note, for example, that this is allowed:

>  bar : Bool → Set1
>  bar b = Set

>  data foo : let x = true in bar x where
>    baz : foo

Here bar computes down to Set.

More generally, it works if there are also
some arguments. This can be useful for abbreviating
complicated definitions. It's probably more useful
for abbreviating constructor types rather than the
type of a new data type, but this does typecheck:

module test where
open import Data.Nat

Rel : Set → Set₁
Rel A = A → A → Set

data Term : Set where

data NStepReduction : ℕ → Rel Term where


More information about the Agda mailing list