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 currency.swift
import Foundation
protocol Currency { static var sign: String { get } }
enum GBP: Currency { static let sign = "£" }
enum EUR: Currency { static let sign = "" }
enum USD: Currency { static let sign = "$" }
protocol _Money {
associatedtype C: Currency
var amount: NSDecimalNumber { get }
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 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.