[Agda] how to type this?

[Nils Anders Danielsson]

On 2009-10-02 18:43, Anton Setzer wrote:
>> module testFunctionDependingOnManyArguments where

Someone wanted to see a version of this code which uses ∞ instead of
codata:

  module testFunctionDependingOnManyArguments where

  open import Coinduction
  open import Data.Nat
  open import Data.Fin as Fin using (Fin; zero; suc)

  data MultiArgsType : Set₁ where
    _∷_ : (X : Set) (F : X → ∞₁ MultiArgsType) → MultiArgsType

  Head : MultiArgsType → Set
  Head (X ∷ F) = X

  Tail : (A : MultiArgsType) → Head A → MultiArgsType
  Tail (X ∷ F) x = ♭₁ (F x)

  data Input (A : MultiArgsType) : Set where
    _∷_ : (x : Head A) (i : ∞ (Input (Tail A x))) → Input A

  X : ℕ → MultiArgsType
  X n = Fin n ∷ λ k → ♯₁ X (n + Fin.toℕ k)

  example : (n : ℕ) → Input (X (suc n))
  example n = zero ∷ (♯ example (n + 0))

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.