Agda-2.3.2.2: test/succeed/CoinductiveAfterEvaluation.agda

module CoinductiveAfterEvaluation where

open import Common.Coinduction

data Functor : Set where
  Id : Functor

_·_ : Functor → Set → Set
Id · A = A

data ν (F : Functor) : Set where
  inn : ∞ (F · ν F) → ν F

-- Evaluation is required to see that Id · ν Id is a coinductive type.

foo : ∀ F → F · ν F
foo Id = inn (♯ foo Id)