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 fold.agda
module Fold where
open import Level using (_⊔_)
open import Data.Nat asusing (ℕ; suc; zero; _+_)
open import Data.List hiding (sum)
open import Relation.Binary.PropositionalEquality
record Fold {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
field
⟦_⟧[] : B
View classical.agda
open import Data.Empty
open import Relation.Nullary
infix 0 ⌊_⌋
⌊_⌋ : {a} Set a Set a
⌊ A ⌋ = ¬ ¬ A
pure : {a} {A : Set a} A ⌊ A ⌋
pure x = λ z z x
View mod-arith.agda
module Scratch where
open import Data.Nat asusing (ℕ; suc; zero)
open import Data.Product
open import Function
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Empty
module GTE where
View builtin-fast-compare.agda
module Data.Nat.Order.Builtin where
open import Data.Nat asusing (ℕ; suc; zero; Ordering; less; equal; greater)
open import Agda.Builtin.Nat using (_-_; _<_; _==_; _+_)
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe
less-hom : n m ((n < m) ≡ true) m ≡ suc (n + (m - n - 1))
less-hom zero zero ()
View NatLiteral.agda
module NatLiteral where
open import Data.Nat asusing (ℕ; suc; zero)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Unit
record Literal (A : Set) : Set₁ where
field
bounds : Set
View zipfix.hs
zipo :: Functor f => (f (Fix f -> a) -> f (Fix f) -> a) -> Fix f -> Fix f -> a
zipo alg = c where c = (\x -> alg x . unfix) . fmap c . unfix
newtype Fix f = Fix (f (Fix f))
unfix :: Fix f -> f (Fix f)
unfix (Fix f) = f
View zipo.hs
import Data.Functor.Foldable
zipo :: (Recursive f, Recursive g)
=> (Base f (g -> c) -> Base g g -> c)
-> f -> g -> c
zipo alg xs = cata (\x -> alg x . project) xs
zipoFix :: Functor f => (f (Fix f -> a) -> f (Fix f) -> a) -> Fix f -> Fix f -> a
zipoFix = zipo
View chunker.py
from itertools import islice, chain
class Chunk:
def __init__(self, iterator, size):
self._iterator = chain([next(iterator)], islice(iterator, size-1))
def __next__(self):
return next(self._iterator)
View trie.hs
{-# options_ghc -Wall #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
View runtimerep.hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
You can’t perform that action at this time.