Skip to content

Instantly share code, notes, and snippets.

Avatar

Donnacha Oisín Kidney oisdk

View GitHub Profile
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 as ℕ using (ℕ; suc; zero)
open import Agda.Primitive using (Level)
open import Cubical.Foundations.Function
variable
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))
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 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
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
You can’t perform that action at this time.