Skip to content

Instantly share code, notes, and snippets.

Avatar

日比野 啓 (Kei Hibino) khibino

View GitHub Profile
View polySum.hs
{-# 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
-- 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
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
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
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
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
{--# 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
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
@khibino
khibino / MetaTheory.agda
Last active Oct 17, 2020
Meta-Theory à la Carte using Agda
View MetaTheory.agda
-- Example implementation for Meta-Theory à la Carte
-- data Fix (f : Set -> Set) : Set where
-- inF : f (Fix f) -> Fix f
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat
View galaxy.hs
f1029 = [7, 123229502148636]
f1030 = [2, 7]
f1031 = [4, 21855]
f1032 = [7, 560803991675135]
f1034 = [5, 33554431]