Basic unit type:
λ> replTy "()"
() :: ()
Basic functions:
Basic unit type:
λ> replTy "()"
() :: ()
Basic functions:
module Main where | |
import IO.Primitive as Prim | |
open import Coinduction | |
open import Data.Unit | |
open import IO | |
cat : IO ⊤ | |
cat = ♯ getContents >>= (\cs → ♯ (putStr∞ cs)) |
{-# OPTIONS --copatterns #-} | |
module Main where | |
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns | |
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600). | |
open import Data.Nat | |
open import Data.Unit | |
open import Data.Bool | |
open import Data.Char |
module Category where | |
open import Agda.Primitive public | |
using (Level ; _⊔_ ; lzero ; lsuc) | |
open import Agda.Builtin.Equality public | |
using (_≡_ ; refl) | |
record Category ℓ ℓ′ : Set (lsuc (ℓ ⊔ ℓ′)) where |
open import Function | |
open import Data.Nat | |
open import Data.Fin renaming (_+_ to _f+_) | |
open import Data.Unit | |
open import Relation.Binary.PropositionalEquality | |
open import Data.Product | |
open import Data.Sum | |
open import Data.Vec | |
open import Data.Vec.Properties |
open import Data.Nat as Nat | |
module Irrelevance-Issue (someMax₁ : ℕ) where | |
open import Level using () renaming ( _⊔_ to _⊔ₗ_) | |
open import Function | |
open import Data.Fin as Fin renaming (_≟_ to _≟f_) | |
hiding (_<_; _≤_; _+_) | |
open import Data.Product as Product |
(defun lapply (fn x a) | |
(cond ((atom fn) (cond ((eq fn 'car) (caar x)) | |
((eq fn 'cdr) (cdar x)) | |
((eq fn 'cons) (cons (car x) (cadr x))) | |
((eq fn 'atom) (atom (car x))) | |
((eq fn 'eq) (eq (car x) (cadr x))) | |
((eq fn 'read) (read)) | |
(t (lapply (leval fn a) x a)))) | |
((eq (car fn) 'lambda) (leval (caddr fn) (pairlis (cadr fn) x a))) | |
((eq (car fn) 'label) (lapply (caddr fn) (cons (cons (cadr fn) |
module Choose where | |
open import Data.Product using (_,_ ; proj₁ ; proj₂ ; ∃) renaming (_×_ to _∧_) | |
open import Relation.Binary.PropositionalEquality using (_≡_ ; sym ; subst) | |
open import Relation.Nullary using (¬_) | |
infix 0 _⇔_ | |
_⇔_ : Set → Set → Set | |
A ⇔ B = (A → B) ∧ (B → A) |
module Prime where | |
open import Codata.Musical.Notation | |
using (∞ ; ♯_ ; ♭) | |
open import Codata.Musical.Stream | |
using (_∷_ ; Stream) | |
open import Data.Empty | |
using (⊥ ; ⊥-elim) |