Skip to content

Instantly share code, notes, and snippets.

Donnacha Oisín Kidney oisdk

Block or report user

Report or block oisdk

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View taba.hs
{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators #-}
import Data.Kind
import Data.Coerce
data Nat = Z | S Nat
data Vec (a :: Type) (n :: Nat) where
Nil :: Vec a Z
(:-) :: a -> Vec a n -> Vec a (S n)
View catalan.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFoldable, DeriveTraversable, DeriveFunctor #-}
import Data.List (mapAccumL)
data Stream a = a :< Stream a deriving (Functor, Foldable, Traversable)
infixr 5 :<
instance Show a => Show (Stream a) where
showsPrec n = showsPrec n . foldr (:) []
View brauntolist.hs
import Test.QuickCheck
import Data.Tree.Binary.Preorder (Tree(..), drawTree)
import Control.Arrow (first)
import Data.List (unfoldr)
fromList :: [a] -> Tree a
fromList xs = head (l (foldr f b xs 1 2))
b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
View ids.hs
{-# LANGUAGE DeriveFunctor, LambdaCase, BlockArguments, BangPatterns, RankNTypes, GeneralisedNewtypeDeriving, OverloadedLists, TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
import Control.Monad
import Control.Applicative
import Numeric.Natural
import GHC.Exts
import GHC.Base (build)
View matrix.hs
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-}
{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}
import Data.Monoid (Sum(..))
import Data.Kind (Type)
data Nat = Z | S Nat
data Fin (n :: Nat) where
View curry.agda
{-# OPTIONS --cubical --safe #-}
module Curry where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
View infnat.agda
data ω : Type₀ where
zero : ω
suc : ω ω
inf : ω
suc-inf : suc inf ≡ inf
ω′ : Type₀
ω′ = Maybe ℕ
zero′ : ω′
View init.hs
init :: [a] -> [a]
init xs = foldr f b xs Nothing
b Nothing = error "init: empty list"
b _ = []
f x xs Nothing = xs (Just x)
f y xs (Just x) = x : xs (Just y)
View lens.agda
{-# OPTIONS --safe --without-K #-}
module Bits where
infixr 4 _×_ _,_
record _×_ (A : Set) (B : Set) : Set where
constructor _,_
fst : A
snd : B
View bfe.agda
{-# OPTIONS --safe --sized-types #-}
module Bits where
open import Agda.Primitive using (Level)
open import Agda.Builtin.Size
a : Level
b : Level
You can’t perform that action at this time.