View FinVector-cons.agda
module FinVector-cons (T : Set) where | |
data Nat : Set where | |
zero : Nat | |
suc : Nat → Nat | |
data Fin : Nat → Set where | |
zero : ∀ {n} → Fin (suc n) | |
suc : ∀ {n} → Fin n → Fin (suc n) |
View extract.py
#!/usr/bin/env python | |
from os import listdir | |
from os.path import isfile, join | |
import re | |
import json | |
from bs4 import BeautifulSoup | |
""" |
View SelectiveSigma.hs
{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-} | |
-- Lots of ways you can phrase this, but this works for me | |
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum. | |
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to | |
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data | |
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the | |
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way | |
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such | |
-- cases, it's often easier to think of this as the essence of existential types. |
View Instances.hs
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ExistentialQuantification #-} | |
module Instances where | |
data Map o k v = Map | |
{ mapOrder :: k -> k -> Ordering | |
, mapImpl :: () -- You'd stick your actual map implementation as another field here and hide the constructor | |
} | |
data ForgottenMap k v = forall o. ForgottenMap (Map o k v) |
View Ack.agda
module Ack where | |
-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties | |
data Nat : Set where | |
zero : Nat | |
suc : Nat → Nat | |
{-# BUILTIN NATURAL Nat #-} |
View FingerStar.agda
module FingerStar where | |
open import Level using (_⊔_) | |
open import Algebra | |
open import Data.Empty | |
open import Data.Product hiding (map) | |
open import Data.Nat hiding (compare; _⊔_) | |
open import Data.Nat.Properties | |
open import Data.Vec renaming (map to mapVec) hiding ([_]) |
View Relations.agda
-- See also https://gist.github.com/copumpkin/2636229 | |
module Relations where | |
open import Level | |
open import Function | |
open import Algebra | |
open import Data.Empty | |
open import Data.Sum as Sum | |
open import Data.Product as Prod | |
open import Relation.Binary |
View classifiers
[箇 个 [ge4] /variant of 個|个[ge4]/,個 个 [ge4] /individual/this/that/size/classifier for people or objects in general/] | |
鼻子 鼻子 [bi2 zi5] /nose/CL:個|个[ge4],隻|只[zhi1]/ | |
鼓舞 鼓舞 [gu3 wu3] /heartening (news)/boost (morale)/CL:個|个[ge4]/ | |
黨員 党员 [dang3 yuan2] /political party member/CL:名[ming2],位[wei4],個|个[ge4]/ | |
黨 党 [dang3] /party/association/club/society/CL:個|个[ge4]/ | |
黑板 黑板 [hei1 ban3] /blackboard/CL:塊|块[kuai4],個|个[ge4]/ | |
黃鱔 黄鳝 [huang2 shan4] /swamp eel/finless eel/CL:個|个[ge4],條|条[tiao2]/ | |
鬼 鬼 [gui3] /ghost/sly/crafty/CL:個|个[ge4]/ | |
高麗菜 高丽菜 [gao1 li4 cai4] /cabbage/CL:顆|颗[ke1],個|个[ge4]/ | |
高度 高度 [gao1 du4] /height/altitude/elevation/high degree/highly/CL:個|个[ge4]/ |
View Resource.hs
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE LiberalTypeSynonyms #-} | |
{-# LANGUAGE ImplicitParams #-} | |
{-# LANGUAGE NoImplicitPrelude #-} | |
{-# LANGUAGE RebindableSyntax #-} | |
module Resource where |
View RuntimeTypes.agda
module RuntimeTypes where | |
open import Function | |
open import Data.Unit | |
open import Data.Bool | |
open import Data.Integer | |
open import Data.String as String | |
open import Data.Maybe hiding (All) | |
open import Data.List | |
open import Data.List.All |
NewerOlder