{{ message }}

Instantly share code, notes, and snippets.

# Donnacha Oisín Kidneyoisdk

Created Oct 15, 2020
View ReductionProblem.agda
 {-# OPTIONS --without-K #-} module ReductionProblem where open import Agda.Builtin.Nat using (Nat; suc; zero) open import Agda.Primitive using (_⊔_) open import Agda.Builtin.Equality using (_≡_; refl) -- The Acc type, defined as a record: record Acc {a r} {A : Set a} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where
Created Sep 17, 2020
View container.hs
 {-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE UndecidableInstances #-} import Data.Kind import Data.Functor.Const
Created Apr 22, 2020
View selective-countable.hs
 -- Selective lets us do "monadic" binds where the domain is restricted -- to the countable types (which can be infinite). {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} import GHC.Generics
Last active Feb 12, 2020
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)
Created Jan 28, 2020
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 (:) []
Created Jan 26, 2020
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)) where b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
Last active Dec 29, 2019
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)
Created Dec 27, 2019
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
Created Dec 15, 2019
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
Created Oct 29, 2019
View infnat.agda
 data ω : Type₀ where zero : ω suc : ω → ω inf : ω suc-inf : suc inf ≡ inf ω′ : Type₀ ω′ = Maybe ℕ zero′ : ω′
You can’t perform that action at this time.