2
module OverloadedConstructors where
8
data Fin : Nat -> Set where
9
zero : {n : Nat} -> Fin (suc n)
10
suc : {n : Nat} -> Fin n -> Fin (suc n)
13
three = suc (suc (suc zero))
22
{-# BUILTIN NATURAL Nat #-}
23
{-# BUILTIN ZERO zero #-}
24
{-# BUILTIN SUC suc #-}