Instantly share code, notes, and snippets.

# Xia Li-yaoLysxia

• Sort options
Created Nov 7, 2019
Trivial example of rewrite with non-transitive relation
View Rw.v
 From Coq Require Import Setoid Morphisms. Inductive Trivial (n : nat) : Prop := T. Definition neq : nat -> nat -> Prop := fun n m => n <> m. Lemma neq_0_1 : neq 0 1. Proof. discriminate.
Last active Nov 5, 2019
View A.hs
 data Robot = Robot Bearing Coordinates deriving (Eq, Show) data Bearing = North | South | East | West deriving (Eq, Show) left :: Bearing -> Bearing left North = West left West = South left South = East left East = North
Created Oct 30, 2019
View dependenttypesftw.v
 Definition nat_eqb (x y : nat) : {x = y} + {x <> y}. Proof. decide equality. Defined. Definition choose (x y : nat) := if nat_eqb x y then 1 else 2. Definition lem {x y : nat} (P : x = y -> False) : choose x y = 2 := match nat_eqb x y as e return (if e then _ else _) = _ with | left r => match P r with end
Last active Oct 28, 2019
Half-verify alternative version of monad laws
View cont.v
 Parameter m : Type -> Type. Notation c r a := ((a -> m r) -> m r). Parameter lift : forall r a, m a -> c r a. Arguments lift {r a}. Parameter pure : forall a, a -> m a. Arguments pure {a}. Definition unlift {a} : c a a -> m a := fun u => u pure.
Created Oct 8, 2019
View Func.hs
 data FuncResult = Ok Integer | NameErr | ArityErr Integer resultOf :: String -> [Integer] -> FuncResult resultOf = applyFuncs [ Func ["D", "derangement", "derangements"] (Arity1 (\n -> derangementR !! fromInteger n)) , Func ["!", "factorial"] (Arity1 factorial) , Func ["g", "gcd", "euclidean"] (Arity2 gcd) , Func ["p", "P", "partition"] (Arity2 partition) , Func ["s", "S", "sterling"] (Arity2 sterling) , Func ["c", "C", "ncr", "combinations"] (Arity2 ncr)
Last active Oct 5, 2019
Initial/final encodings of initial/final (co)algebras
View IFIF.hs
 {- Initial/final encodings of initial/final (co)algebras -} {-# LANGUAGE GADTs, KindSignatures, RankNTypes #-} module IFIF where import Data.Kind (Type) -- Initial encoding of the initial algebra of f
Created Oct 3, 2019
Indexed containers for game semantics
View HTree.v
 (** An (indexed) "container" encodes an indexed recursive type. *) (** A container can also be seen as a game, with - [ix] as the type of positions, - [shape i] the Player moves at position [i], - [pos i s] the Opponent moves after Player plays move [s] on position [i], - [posix i s p] the new position after moves [s] and [p] from position [i]. *) Module Export Container. Record container :=
Last active Sep 25, 2019
View containers.v
 Set Implicit Arguments. Set Contextual Implicit. Record container : Type := { shape : Type; pos : shape -> Type; }. Inductive ext (c : container) (a : Type) : Type := { this_shape : shape c;
Last active Sep 18, 2019
View GFunctor.hs
 class GFunctor (p :: c -> c -> *) (q :: d -> d -> *) (f :: c -> Exp d) where gfmap :: p x y -> q (f @@ x) (f @@ y) instance (GFunctor p q f, GFunctor q r g) => GFunctor p r (g . f) where gfmap = gfmap @q @r @g . gfmap @p @q @f data (.) :: (d -> Exp e) -> (c -> Exp d) -> (c -> Exp e) type instance Eval ((f . g) x) = Eval (f (Eval (g x))
Last active Sep 18, 2019
View E.hs
 type Lets = Exp -> Exp -- "Stack of lets", functions of this form: -- (Let b1 . Let b2 . ... . Let bn) snoc :: Lets -> (Var, Exp) -> Lets snoc k b = k . Let b type M = State (T.Text, Int, Lets) push :: (Var, Exp) -> M Exp
You can’t perform that action at this time.