Skip to content

Instantly share code, notes, and snippets.

View Sorting.agda
module Sorting where
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary
@gallais
gallais / pragmabug
Created Nov 18, 2013
Underscore in a pragma breaks the lhs2tex-generated LaTeX code
View pragmabug
\documentclass{article}
%include lhs2TeX.fmt
%include lhs2TeX.sty
%include polycode.fmt
\begin{document}
\begin{code}
module Equal where
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
View Nsatz Complex
Require Import Complex Cpow Ctacfield.
Require Import Nsatz.
Lemma Csth : Setoid_Theory C (@eq C).
constructor;red;intros;subst;trivial.
Qed.
Instance Cops: (@Ring_ops C C0 C1 Cadd Cmult Cminus Copp (@eq C)).
@gallais
gallais / Disjunctive.agda
Created Apr 17, 2014
Disjunctive normal form
View Disjunctive.agda
module Disjunctive where
open import Data.Product
import Data.Bool as 𝔹
open import Data.Bool.Properties
open import Data.Nat
open import Data.Fin
open import Data.Vec hiding ([_])
open import Algebra.Structures
@gallais
gallais / lte10
Created May 2, 2014
Auto-convert
View lte10
module lte10 where
open import Data.Empty
open import Data.Unit
open import Data.Nat as ℕ
open import Data.Maybe
open import Data.Vec
open import Function
View NoMono
{-# LANGUAGE GADTs#-}
data Lam a where
Var :: a -> Lam a
App :: Lam a -> Lam a -> Lam a
Lam :: Lam (Maybe a) -> Lam a
mapLam :: (a -> b) -> Lam a -> Lam b
mapLam f (Var a) = Var $ f a
mapLam f (App t u) = mapLam f t `App` mapLam f u
View sum_of_pow.v
Require Import NArith.
Fixpoint sum_of (f : nat -> nat) (n : nat) : nat :=
match n with
| O => f O
| S m => f (S m) + sum_of f m
end.
Lemma sum_of_pow : forall n,
S (sum_of (NPeano.pow 2) n) = NPeano.pow 2 (S n).
View Morse decoder.hs
module Main where
data Trie a =
Leaf
| Node (Trie a) a (Trie a)
data Code = Dot | Dash
type Word = [ Code ]
type Phrase = [ Word ]
type Dict = Trie (Maybe Char)
@gallais
gallais / Fam.agda
Last active Aug 29, 2015
Categories.Fam generalized
View Fam.agda
module Categories.Fam where
open import Level
import Function as Fun
open import Data.Product
open import Relation.Binary
open import Categories.Category
open import Categories.Support.EqReasoning
open import Categories.Support.PropositionalEquality
View LEM.hs
{-# LANGUAGE DeriveDataTypeable #-}
module LEM where
import Control.Exception
import Data.Typeable
import System.IO.Unsafe
data Void