View Session10.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- Conceptual Mathematics, Session 10, exercises -} | |
module Session10 where | |
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; _≢_) | |
open import Data.Product using (∃; _,_; _×_) | |
open import Relation.Nullary using (¬_) | |
-- contraposition : ∀ {l} -> ∀ {A B : Set l} -> (A -> B) -> ¬ B -> ¬ A | |
-- contraposition f nb a = nb (f a) |
View div.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Agda.Builtin.Equality using (_≡_; refl) | |
open import Relation.Binary.PropositionalEquality.Core using (sym; trans; _≢_) | |
-- open import Data.Nat.Base | |
open import Data.Nat.Base | |
using (ℕ; zero; suc; _+_; _*_; s≤s; z≤n; _≤_; _<_; _>_; | |
Ordering; less; equal; greater; compare) | |
open import Data.Nat.Properties using (+-identityʳ; +-assoc; ≤-trans; m≤m+n; m≢1+m+n; *-cancelˡ-≡) | |
open import Data.Empty using (⊥) | |
open import Relation.Nullary using (¬_) | |
open import Data.Product using (_×_; _,_) |
View polySum.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses, | |
FunctionalDependencies, FlexibleInstances, FlexibleContexts, | |
OverloadedLabels, ScopedTypeVariables #-} | |
import GHC.OverloadedLabels (IsLabel(..)) | |
import GHC.TypeLits (Symbol) | |
data Label (l :: Symbol) = Put | |
class Belongs a l b | l b -> a where |
View format.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- printf like function, formatting package method | |
newtype Format r a = Format ((ShowS -> r) -> a) | |
string :: Format r (String -> r) | |
string = Format $ \k s -> k (s ++) | |
int :: Format r (Int -> r) | |
int = Format $ \k i -> k (show i ++) |
View ListMonad.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Function.Base using (_∘_) | |
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) | |
---------- | |
-- List の定義 | |
infixr 50 _∷_ | |
data List (A : Set) : Set where | |
[] : List A |
View set1.agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Agda.Primitive using (lsuc) | |
open import Data.Bool using (Bool) | |
Fix : ∀{l} -> (Set l → Set l) → Set (lsuc l) | |
Fix f = ∀ k → (f k → k) → k | |
T : ∀{l} → Set l → Set l | |
T a = (a → Bool) → Bool | |
X : Set1 |
View bin2.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem plus_0_r : forall n:nat, n + 0 = n. | |
Proof. | |
intros n. induction n as [| n']. | |
(* Case "n = 0". *) + reflexivity. | |
(* Case "n = S n'". *) + simpl. rewrite -> IHn'. reflexivity. Qed. | |
(** 練習問題: ★★★★, recommended (binary) *) | |
(* (a) *) | |
Inductive bin : Type := |
View bin.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem plus_0_r : forall n:nat, n + 0 = n. | |
Proof. | |
intros n. induction n as [| n']. | |
(* Case "n = 0". *) + reflexivity. | |
(* Case "n = S n'". *) + simpl. rewrite -> IHn'. reflexivity. Qed. | |
(** **** 練習問題: ★★★★, recommended (binary) *) | |
(** これまでとは異なる、通常表記の自然数ではなく2進のシステムで、自然数のより効率的な表現を考えなさい。それは自然数をゼロとゼロに1を加える加算器からなるものを定義する代わりに、以下のような2進の形で表すものです。2進数とは、 | |
- ゼロであるか, | |
- 2進数を2倍したものか, |
View prunner.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{--# OPTIONS_GHC -Wno-name-shadowing #-} | |
import Control.Concurrent (forkIO) | |
import Control.Concurrent (threadDelay) | |
import Control.Concurrent.Chan (Chan, newChan, readChan, writeChan) | |
import Control.Monad (void, replicateM, replicateM_) | |
import System.IO (BufferMode (LineBuffering), hSetBuffering, stdout) | |
----- |
View Language.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Language where | |
import Utils | |
import Prelude hiding (seq) | |
data Expr a | |
= EVar Name -- ^ Variables | |
| ENum Int -- ^ Numbers | |
| EConstr Int Int -- ^ Constructor tag arity | |
| EAp (Expr a) (Expr a) -- ^ Applications |
NewerOlder