Skip to content

Instantly share code, notes, and snippets.

View gallais's full-sized avatar

G. Allais gallais

328 followers · 147 following
View GitHub Profile
@gallais
gallais / ShowBoth.hs
Created November 3, 2016 13:15
Show Both in Haskell (cf. https://gist.github.com/Qqwy/e092a68d508268f0f25cb5d1ffb3ad72)
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ShowBoth where
import Data.Proxy
@gallais
gallais / Fibonaccis.v
Created November 13, 2016 17:47
Fibonacci cooked 2 ways
Require Import NArith.
Fixpoint fac_v1 (n : nat) : nat :=
match n with
| 0 => 1
| S n' => n * (fac_v1 n')
end.
Fixpoint visit_fac_v2 (n a : nat) : nat :=
match n with
@gallais
gallais / StringNat.agda
Created November 21, 2016 23:24
module StringNat where
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Data.Unit
open import Data.Bool
open import Data.Product
open import Function
data CharView : Char → Set where
@gallais
gallais / star_lemma.v
Last active November 25, 2016 19:30
Star lemma
Set Implicit Arguments.
Require Import Ascii String.
Inductive regex : Set :=
| Emp : regex
| Eps : regex
| Chr : ascii -> regex
| Cat : regex -> regex -> regex
| Choice : regex -> regex -> regex
@gallais
gallais / UntypedLambda.v
Created December 4, 2016 21:42
Interpreting the untyped lambda calculus in Coq (cf. https://gist.github.com/gallais/303cfcfe053fbc63eb61 for Agda)
Inductive Fin : nat -> Type :=
| Zero : forall n, Fin (S n)
| Succ : forall n, Fin n -> Fin (S n)
.
Arguments Zero [n].
Arguments Succ [n] k.
Inductive Expr (n : nat) : Type :=
@gallais
gallais / IfThenElse.hs
Created February 15, 2017 12:34
Getting a type-level ITE to fire
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Ite where
import Data.Proxy
import GHC.TypeLits
@gallais
gallais / Even.agda
Created February 21, 2017 11:30
Alternative definition of Even
module Even where
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
data Even : ℕ → Set where
@gallais
gallais / UIP.agda
Last active February 25, 2017 17:44
eq-dec => UIP proof taken from https://sympa.inria.fr/sympa/arc/coq-club/2016-09/msg00064.html
{-# OPTIONS --without-K #-}
module UIP where
open import Level
open import Relation.Binary.PropositionalEquality
record Canonical {ℓ} {ℓ′} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
field canonical : A → B
constraint : ∀ a a′ → canonical a ≡ canonical a′
@gallais
gallais / ModularParser2.hs
Last active March 1, 2017 00:41
Trying to see what Ptival's Modular Parser would look like for mutually defined types of expressions
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
@gallais
gallais / ModularParser3.hs
Last active March 1, 2017 00:43
Trying to see what Ptival's Modular Parser would look like for mutually defined types of expressions
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module ModularParser3 where
import Data.Function