This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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} [] ≡ [] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 _≣_) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 | |
-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE LiberalTypeSynonyms #-} | |
{-# LANGUAGE ImplicitParams #-} | |
{-# LANGUAGE NoImplicitPrelude #-} | |
{-# LANGUAGE RebindableSyntax #-} | |
module Resource where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 ([_]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <iostream> | |
void f(int &imachangeu) { | |
imachangeu = 7; | |
} | |
int main() { | |
int x = 5; | |
std::cout << x << std::endl; | |
OlderNewer