cutsea110

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE RankNTypes #-}
module Test where

data X = X String 
       deriving Show
                
type Y = Int

class Z a where

cutsea110

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
module Test where

data X = X String 
       deriving Show
                
type Y = Int

cutsea110

{-# LANGUAGE FlexibleInstances, ImplicitParams #-}
import Control.Monad
import Control.Applicative

instance (Monad m, Num b) => Num (a -> m b) where
  a + b =  liftM2 (+) <$> a <*> b
  a * b = liftM2 (*) <$> a <*> b
  negate a = liftM negate <$> a
  abs a = liftM abs <$> a
  signum a = liftM signum <$> a

cutsea110

{-# LANGUAGE NoMonomorphismRestriction #-}
module Test where

import Control.Applicative ((<$>),(<*>))
import Control.Monad.State (get, put, lift, StateT(..))
import Control.Monad.Trans.Either (right, left, EitherT(..))

type C a = EitherT String (StateT [a] IO)

-- low level

cutsea110

ex-1-3-1 : ∀ {n₁ n₂ n₃} → (p : n₁ plus n₂ is n₃) → steps-plus p ≡ 1 + n₁
ex-1-3-1 P-Zero = refl
ex-1-3-1 (P-Succ p) = cong S (ex-1-3-1 p)

ex-1-3-2 : ∀ {n₁ n₂ n₃} → (p : n₁ times n₂ is n₃) → steps-times p ≡ 1 + n₁ * (n₂ + 2)
ex-1-3-2 T-Zero = refl
ex-1-3-2 (T-Succ t p) = cong S (plus+times≡n₂+2+n₁[n₂+2] t p)
  where
    S[a+Sb]≡a+2+b : (a b : ℕ) → S (a + S b) ≡ a + 2 + b
    S[a+Sb]≡a+2+b Z b = refl

cutsea110

module Test where

open import Data.Bool
open import Data.Char hiding (_==_)
open import Data.String hiding (_==_)

record Eq (A : Set) : Set₁ where
  field
    _==_ : A → A → Bool

cutsea110

-- theorem 2.5
associativity-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₁ plus n₂ is n₄ → n₄ plus n₃ is n₅ →
                     ∃ λ n₆ → n₂ plus n₃ is n₆ → n₁ plus n₆ is n₅
associativity-plus {Z} {Z} {Z} {Z} {Z} P-Zero P-Zero = Z , (λ x → x)
associativity-plus {Z} {Z} {Z} {Z} {S n₅} P-Zero ()
associativity-plus {Z} {Z} {Z} {S n₄} {Z} () l₂
associativity-plus {Z} {Z} {Z} {S n₄} {S n₅} () l₂
associativity-plus {Z} {Z} {S n₃} {Z} {Z} P-Zero ()
associativity-plus {Z} {Z} {S n₃} {Z} {S .n₃} P-Zero P-Zero = S n₃ , (λ x → x)
associativity-plus {Z} {Z} {S n₃} {S n₄} {Z} () l₂

cutsea110

-- theorem 2.5
associativity-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₁ plus n₂ is n₄ → n₄ plus n₃ is n₅ →
                     ∃ λ n₆ → n₂ plus n₃ is n₆ → n₁ plus n₆ is n₅
associativity-plus {Z} {Z} {Z} {Z} {Z} P-Zero P-Zero = Z , id
associativity-plus {Z} {Z} {Z} {Z} {S n₅} P-Zero ()
associativity-plus {Z} {Z} {n₄ = S n₄} () l₂
associativity-plus {Z} {Z} {S n₃} {Z} {Z} P-Zero ()
associativity-plus {Z} {Z} {S n₃} {Z} {S .n₃} P-Zero P-Zero = S n₃ , id
associativity-plus {Z} {S n₂} {n₄ = Z} () l₂
associativity-plus {Z} {S n₂} {n₄ = S .n₂} {n₅ = Z} P-Zero ()

cutsea110

module kyoin-test where

open import Data.Bool.Properties
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Coprimality as Coprime
open import Data.Nat.Divisibility
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Sum

cutsea110

module ex where

open import Level using (Level) renaming (suc to lsuc)
open import Data.Bool using (Bool; true; false)
open import Data.Nat
open import Data.Maybe using (Maybe; just; nothing)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_)
open import Relation.Nullary using (Dec; yes; no)
open import Data.Unit using (⊤; tt)