View Reverse.agda
module Reverse where | |
open import Data.List as List hiding (reverse) | |
open import Data.List.Properties | |
open import Relation.Binary.PropositionalEquality | |
record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where | |
constructor rl | |
field | |
reverse0 : ∀ {A} → reverse {A} [] ≡ [] |
View Cont.agda
module Categories.Agda.Cont where | |
open import Categories.Category | |
open import Categories.Agda | |
open import Categories.Functor | |
open import Categories.Monad | |
open import Categories.Adjunction | |
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≣_) |
View Mat.agda
module Mat where | |
open import Function | |
open import Data.Empty | |
open import Data.Nat using (ℕ; zero; suc) | |
open import Data.Fin using (Fin; zero; suc; toℕ) | |
open import Data.Fin.Props using () | |
open import Data.Product | |
open import Relation.Nullary | |
open import Relation.Binary |
View Prickler.hs
{-# LANGUAGE TemplateHaskell, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-} | |
module Prickler where | |
{- | |
Main goals: | |
# Minimal indirection, so I didn't want big n-tuples of stuff getting curried into constructors or shit like that | |
# Magical constructor/eliminator pairing, so I don't have to write ugly unsafe pattern matches or constructor -> Int mappings (unlike the alt combinator in the pickler paper) | |
# Minimize the amount of metadata traversal that happens during serialization (not 100% there yet) | |
# Not be ugly to use | |
-} |
View Format.hs
{-# LANGUAGE EmptyDataDecls, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-} | |
module Format where | |
import Prelude hiding (read) | |
import Data.Either | |
import Data.Binary.Get | |
import Data.Binary.Builder | |
import Data.Monoid | |
import Data.Foldable | |
import Control.Applicative |
View Resource.hs
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE LiberalTypeSynonyms #-} | |
{-# LANGUAGE ImplicitParams #-} | |
{-# LANGUAGE NoImplicitPrelude #-} | |
{-# LANGUAGE RebindableSyntax #-} | |
module Resource where |
View FingerStar.agda
module FingerStar where | |
open import Level using (_⊔_) | |
open import Algebra | |
open import Data.Empty | |
open import Data.Product hiding (map) | |
open import Data.Nat hiding (compare; _⊔_) | |
open import Data.Nat.Properties | |
open import Data.Vec renaming (map to mapVec) hiding ([_]) |
View Ack.agda
module Ack where | |
-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties | |
data Nat : Set where | |
zero : Nat | |
suc : Nat → Nat | |
{-# BUILTIN NATURAL Nat #-} |
View Instances.hs
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ExistentialQuantification #-} | |
module Instances where | |
data Map o k v = Map | |
{ mapOrder :: k -> k -> Ordering | |
, mapImpl :: () -- You'd stick your actual map implementation as another field here and hide the constructor | |
} | |
data ForgottenMap k v = forall o. ForgottenMap (Map o k v) |
View gist:93840
#include <iostream> | |
void f(int &imachangeu) { | |
imachangeu = 7; | |
} | |
int main() { | |
int x = 5; | |
std::cout << x << std::endl; | |
OlderNewer