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 DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# OPTIONS_GHC -Wall #-} | |
data HList f l where | |
HNil :: HList f '[] |
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 #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE TypeFamilyDependencies #-} | |
data Ty = IntTy | FunTy Ty Ty |
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 #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE RankNTypes #-} | |
data Ty = IntTy | FunTy Ty Ty | |
data Term :: (Ty -> *) -> Ty -> * where | |
Lit :: Int -> Term var IntTy |
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
theory locale_experiment | |
imports Main | |
begin | |
section \<open>Algebraic formulation of a semilattice\<close> | |
locale semigroup = | |
fixes ap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" | |
assumes assoc: "\<And>x y z. ap x (ap y z) = ap (ap x y) z" |
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
-- Matthew Brecknell @mbrcknl | |
-- BFPG.org, March-April 2015 | |
-- With thanks to Conor McBride (@pigworker) for his lecture series: | |
-- https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87 | |
-- from which I learned most of what I know about Agda, and | |
-- from which I stole several ideas for this talk. | |
open import Agda.Primitive using (_⊔_) |
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
theory Scratch imports Main begin | |
locale Magma = | |
fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" | |
locale SemiGroup = Magma + | |
assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)" | |
locale Commutative = Magma + | |
assumes comm: "\<And>x y. m x y = m y x" |
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
Definition p5 : com := | |
WHILE (BNot (BEq (AId X) (ANum 1))) DO | |
HAVOC X | |
END. | |
Definition p6 : com := | |
X ::= ANum 1. | |
Lemma p5_may_terminate: forall s, p5 / s || update s X 1. | |
intro s; destruct (eq_nat_dec (s X) 1). |
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
import Data.Set.Monad as SM | |
import Debug.Trace as DT | |
(<+>) = liftM . plus | |
plus x y = DT.trace "." (x + y) | |
l = SM.fromList [0,1] | |
-- Intuitively expect 28 additions, but we actually get 60! | |
test = Set Int |
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
# ... | |
if [ -f ~/.gpg-agent-info ]; then | |
. ~/.gpg-agent-info | |
export GPG_AGENT_INFO | |
fi | |
# ... |
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 List. | |
Inductive type : Type := | |
| base : type | |
| arr : type -> type -> type. | |
Infix "==>" := arr (right associativity, at level 52). | |
Inductive elem {A: Type} (x: A): list A -> Type := | |
| here : forall xs, elem x (x :: xs) |
NewerOlder