Skip to content

Instantly share code, notes, and snippets.

View gallais's full-sized avatar

G. Allais gallais

View GitHub Profile
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 / pragmabug
Created November 18, 2013 15:16
Underscore in a pragma breaks the lhs2tex-generated LaTeX code
View pragmabug
%include lhs2TeX.fmt
%include lhs2TeX.sty
%include polycode.fmt
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).
Instance Cops: (@Ring_ops C C0 C1 Cadd Cmult Cminus Copp (@eq C)).
gallais / Disjunctive.agda
Created April 17, 2014 11:46
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 / lte10
Created May 2, 2014 14:55
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
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
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 =
| Node (Trie a) a (Trie a)
data Code = Dot | Dash
type Word = [ Code ]
type Phrase = [ Word ]
type Dict = Trie (Maybe Char)
gallais / Fam.agda
Last active August 29, 2015 14:06
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
gallais / LEM.hs
Last active August 29, 2015 14:06
View LEM.hs
{-# LANGUAGE DeriveDataTypeable #-}
module LEM where
import Control.Exception
import Data.Typeable
import System.IO.Unsafe
data Void