Skip to content

Instantly share code, notes, and snippets.

Matthew Brecknell mbrcknl

Block or report user

Report or block mbrcknl

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View hlist.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wall #-}
data HList f l where
HNil :: HList f '[]
View PHOAS.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}
data Ty = IntTy | FunTy Ty Ty
View PHOAS.hs
{-# 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
View locale_experiment.thy
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"
View Scratch.thy
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"
View sf_p5_p6_equiv.v
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).
View phoas.v
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)
View SortingFunction.v
Require Import Sorted.
Require Import Permutation.
Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).
Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).
@mbrcknl
mbrcknl / phoas-de-bruijn.v
Created Oct 20, 2015
Mucking about with PHOAS and type-indexed de Bruijn representations
View phoas-de-bruijn.v
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)
@mbrcknl
mbrcknl / Norm.v
Created Sep 29, 2015
Extending saturated sets to product types, alternative version
View Norm.v
Fixpoint R (T:ty) (t:tm) {struct T} : Prop :=
has_type empty t T /\ halts t /\
match T with
| TBool => True
| TArrow T1 T2 => (forall s, R T1 s -> R T2 (tapp t s))
| TProd T1 T2 => exists t1, exists t2, t ==>* tpair t1 t2 /\ R T1 t1 /\ R T2 t2
end.
You can’t perform that action at this time.