Skip to content

Instantly share code, notes, and snippets.


Donnacha Oisín Kidney oisdk

View GitHub Profile
treeowl / Bftr.hs
Last active Mar 16, 2020
Breadth-first binary tree creation
View Bftr.hs
-- | This module defines a function that produces a complete binary tree
-- from a breadth-first list of its (internal) node labels. It is an
-- optimized version of an implementation by Will Ness that avoids
-- any "impossible" cases. See
module Bftr (Tree (..), bft, list, deftest) where
import Data.Function (fix)
import Data.Monoid (Endo (..))
View infnat.agda
{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything
open import Cubical.Data.Maybe
open import Cubical.Data.Nat
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
data ω : Type₀ where
inflation / retina.patch
Created Jun 12, 2018
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
AndrasKovacs / TypeLambdas.hs
Last active Sep 23, 2019
Type lambdas and induction with GHC 8.4.2 and singletons
View TypeLambdas.hs
{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
TypeOperators, TypeApplications, AllowAmbiguousTypes,
TypeInType, StandaloneDeriving #-}
import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind
-- some standard stuff for later examples' sake
contra /
Last active Aug 4, 2020
Age of Empires II HD - For Mac OSX

AOE2HD - For Mac OSX

Estimated time: 10 minutes


PlayOnMac does not work on macOS Catalina at all - and on older versions of macOS issues have been reported with the latest version of Steam. Updating is in progress, read more here.

When the updates are released this guide will be updated. Please do not blow up my inbox by leaving comments "WHY DOESNT IT WORK".

treeowl / BasicNat.hs
Last active Jun 30, 2019
Fast total sorting of arbitrary Traversable containers
View BasicNat.hs
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs,
ScopedTypeVariables, TypeOperators #-}
-- | Type-level natural numbers and singletons, with proofs of
-- a few basic properties.
module BasicNat (
-- | Type-level natural numbers
Nat (..)
, type (+)
dysinger / packages.el
Last active Mar 24, 2020
Private spacemacs layer to try out Chris Done's Intero mode for haskell
View packages.el
;; 1. place this in ~/.emacs.d/private/intero/packages.el
;; 2. add intero, syntax-checking and auto-completion to your
;; ~/.spacemacs layer configuration & remove the haskell layer
;; if you were using that before
;; 3. make sure you have stack installed
;; 4. fire up emacs & open up a stack project's source files
View beamer-slides-with-notes.pdf
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
copumpkin / Prime.agda
Last active May 17, 2020
There are infinite primes
View Prime.agda
module Prime where
open import Coinduction
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
open import Data.Fin.Props hiding (_≟_)
You can’t perform that action at this time.