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 |
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 |
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)). |
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 |
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 |
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 |
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). |
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) |
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 |
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 |
OlderNewer