Instantly share code, notes, and snippets.

# 日比野 啓 (Kei Hibino) khibino

Last active January 18, 2023 13:25
Conceptual Mathematics, Session 10, exercises
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)
Last active November 16, 2022 08:25
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 (_×_; _,_)
Created August 26, 2022 07:30
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
Created August 2, 2022 04:06
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 ++)
Last active January 5, 2022 11:12
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
Created December 13, 2021 08:17
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
Created October 6, 2021 13:42
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 :=
Created October 6, 2021 10:57
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倍したものか,
Created September 20, 2021 16:14
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) -----
Last active August 21, 2021 04:05
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