Skip to content

Instantly share code, notes, and snippets.

Donnacha Oisín Kidney oisdk

View GitHub Profile
@oisdk
oisdk / retina.patch
Created Apr 15, 2019 — forked from inflation/retina.patch
Retina support for auctex of emacs-osx-port
View retina.patch
*** preview.el.orig 2018-06-11 14:08:50.000000000 -0400
--- preview.el 2018-06-11 15:35:38.000000000 -0400
***************
*** 180,186 ****
(close preview-gs-close))
(tiff (open preview-gs-open)
(place preview-gs-place)
! (close preview-gs-close)))
"Define functions for generating images.
These functions get called in the process of generating inline
View cnostrained.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
import Prelude hiding ((.), id, Functor)
import Data.Constraint
import Data.Kind
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)
You can’t perform that action at this time.