mietek

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))

mietek

module Brouwer where


-- From Brouwer’s Cambridge lectures on intuitionism (1946-1951):
--
-- “Theorem. Absurdity of absurdity of absurdity is equivalent to absurdity.
--
-- Proof. Firstly, since implication of the assertion y by the assertion x implies
-- implication of absurdity of x by absurdity of y, the implication of absurdity of
-- absurdity by truth (which is an established fact) implies the implication of

mietek

module DecidableOPE where

open import Agda.Primitive using (_⊔_)

data ⊥ : Set where

elim⊥ : ∀ {ℓ} {X : Set ℓ} → ⊥ → X
elim⊥ ()

infix 3 ¬_

mietek

module Prelude where

open import Agda.Primitive public
  using (_⊔_ ; lsuc)


-- Truth.

open import Agda.Builtin.Unit public
  using (⊤)

mietek

module Main where

main :: IO ()
main = do
  str <- getLine
  let x = show (read str)
  putStrLn x

{-
$ ghc -Wall -o foo Main.hs

mietek

open import Data.Maybe using (Maybe ; just)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

bad₁ : {A : Set} {x y : A} → (just x) ≡ (just y) → x ≡ y
bad₁ p = {!!}

bad₂ : ∀ {a} {A : Set a} {x y : A} → (just x) ≡ (just y) → x ≡ y
bad₂ p = {!!}

good₁ : {A : Set} {x y : A} → (Maybe.just x) ≡ (Maybe.just y) → x ≡ y

mietek

module DataCodata where

open import Data.Product using (_×_ ; _,_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)


--------------------------------------------------------------------------------


case : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}

mietek

module Church where

open import Agda.Primitive public using (_⊔_ ; lsuc)


record ⊤ : Set where
  instance
    constructor ∙

infixl 5 _,_

mietek

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

mietek

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}

import Data.String (IsString, fromString)
import GHC.TypeLits (KnownSymbol, Symbol, someSymbolVal, symbolVal)