Instantly share code, notes, and snippets.

G. Allais gallais

Last active May 24, 2018 — forked from twanvl/Sorting.agda
View Sorting.agda
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 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
Created Nov 18, 2013
Underscore in a pragma breaks the lhs2tex-generated LaTeX code
View pragmabug
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
 \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
Created Feb 7, 2014
View Nsatz Complex
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
 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)).
Created Apr 17, 2014
Disjunctive normal form
View Disjunctive.agda
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 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
Created May 2, 2014
Auto-convert
View lte10
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 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
Created May 4, 2014
View NoMono
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 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
Last active Aug 29, 2015
View sum_of_pow.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
 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).
Last active Aug 29, 2015
View Morse decoder.hs
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 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)
Last active Aug 29, 2015
Categories.Fam generalized
View Fam.agda
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.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
Last active Aug 29, 2015
View LEM.hs
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 DeriveDataTypeable #-} module LEM where import Control.Exception import Data.Typeable import System.IO.Unsafe data Void