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 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
where
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 _,_
field
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
variable
a : Level
b : Level
View matrices.agda
{-# OPTIONS --safe --cubical #-}
module Bits where
open import Cubical.Data.Nat asusing (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function
variable
a : Level
View rats.hs
import Numeric.Natural
import Data.Function
-- R a = Fix (ContT a [])
newtype R a = R { r :: (R a -> [a]) -> [a] }
bfUnfold :: (a -> (b,a,a)) -> a -> [b]
bfUnfold f t = g t (fix (R . flip id)) (fix (flip r))
where
g b fw bw = x : r fw (bw . R . g ys . R . g zs)
View isPal.hs
isPal :: forall a. Eq a => [a] -> Bool
isPal xs = getAll (fst (go xs xs)) where
go (y:ys) (_:_:zs) = f y =<< go ys zs
go (_:ys) [_] = pure ys
go ys [] = pure ys
f y ~(z:zs) = (All (y == z), zs)
View dijkstra.hs
{-# LANGUAGE DeriveFunctor, LambdaCase, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, RankNTypes, GeneralizedNewtypeDeriving #-}
import Data.Semigroup hiding (Sum(..))
import Control.Applicative
import Control.Monad
import Data.Functor.Classes
import Control.Monad.State
import qualified Data.Set as Set
import Data.Set (Set)
View tabular.hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
import Data.Semigroup
import Control.Arrow
import Data.Align
import Data.Coerce
import Data.Tuple
newtype Stream a = Stream [a]
View star.hs
{-# LANGUAGE DeriveFunctor, LambdaCase #-}
import Control.Applicative hiding (many)
import Control.Monad
newtype Parser a = Parser { runParser :: String -> [(a, String)] } deriving Functor
instance Applicative Parser where
pure x = Parser (\s -> [(x,s)])
fs <*> xs = fs >>= (\f -> xs >>= (\x -> pure (f x)))
You can’t perform that action at this time.