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 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 Jan 8, 2020
Age of Empires II HD - For Mac OSX

AOE2HD - For Mac OSX

Estimated time: 10 minutes


PlayOnMac does not work on macOS Catalina, and 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.

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 Aug 21, 2019
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 Sep 9, 2019
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.