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 bfe.agda
{-# OPTIONS --safe --sized-types #-}
module Bits where
open import Agda.Primitive using (Level)
open import Agda.Builtin.Size
a : Level
b : Level
View matrices.agda
{-# OPTIONS --safe --cubical #-}
module Bits where
open import Cubical.Data.Nat as ℕ using (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function
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))
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)))
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 as ℕ using (ℕ; 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
You can’t perform that action at this time.