16 lines
304 B
Agda
16 lines
304 B
Agda
|
{-# OPTIONS --guardedness #-}
|
||
|
|
{-# OPTIONS --type-in-type #-}
|
||
|
|
|
||
|
|
module Zdancewic.Monads where
|
||
|
|
|
||
|
|
open import Agda.Primitive
|
||
|
|
open import Data.Nat
|
||
|
|
|
||
|
|
record ITree (E : Set → Set) (R : Set) : Set where
|
||
|
|
coinductive
|
||
|
|
field
|
||
|
|
ret : R
|
||
|
|
tau : ITree E R
|
||
|
|
vis : ∀ {A} → (e : E A) → (A → ITree E R)
|
||
|
|
|