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 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)))
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
⟦_⟧[] : 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
bounds : Set
You can’t perform that action at this time.