Skip to content

Instantly share code, notes, and snippets.

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 / 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
@gallais
gallais / MutuallDefined.hs
Last active Aug 29, 2015
Mutually Defined Datatypes
View MutuallDefined.hs
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
module MutuallyDefined where
import Data.Type.Natural
@gallais
gallais / MutuallyDefinedList.hs
Last active Aug 29, 2015
MutuallyDefinedList
View MutuallyDefinedList.hs
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
module MutuallyDefinedList where
@gallais
gallais / MutuallyDefined.agda
Last active Aug 29, 2015
Mutually Defined Datatypes
View MutuallyDefined.agda
{-# OPTIONS --no-termination-check --no-positivity-check #-}
module MutuallyDefined where
open import Data.Nat as ℕ
open import Data.Fin
open import Function
data Tie {n : ℕ} (F : (Fin n Set) Fin n Set) (k : Fin n) : Set where
⟨_⟩ : (v : F (Tie F) k) Tie F k