Xia Li-yao Lysxia

Lysxia / A.v

Created September 5, 2018 19:05

	Lemma plus_1 : forall n, 1 + n = S n.
	Proof. reflexivity. Qed.

	Lemma f : forall n, S (1 + n) = S (S n).
	Proof. intros n. rewrite plus_1. (* error on the last tactic *)

	(* Error: Tactic generated a subgoal identical to the original goal. *)

Lysxia / A.hs

Created September 16, 2018 14:13

Example using MonadError + CallStack

	{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}

	import Control.Monad.IO.Class
	import Control.Monad.Except
	import GHC.Stack (HasCallStack, CallStack, callStack, prettyCallStack)

	data MyException = MyException CallStack String
	deriving Show

	merror :: (HasCallStack, MonadError MyException m) => String -> m a

Lysxia / A.hs

Created September 24, 2018 17:29

	{-# LANGUAGE TemplateHaskell, DataKinds #-}

	import GHC.Stack

	f :: HasCallStack => Int
	f = error "XXX"

	g :: Int
	g = f

Lysxia / K.hs

Created October 16, 2018 17:15

https://gist.github.com/Synthetica9/2fd591cd4560eed189206e19c8ae3259 as a fold over Free

	{-# LANGUAGE DeriveFunctor, DeriveFoldable, LambdaCase, RankNTypes #-}

	import Data.Functor.Foldable
	import Control.Monad.Free
	import Data.Maybe

	-- original
	superCata
	:: (Functor f, Foldable f)
	=> (r -> r -> r) -> r -> (f r -> Maybe r) -> Fix f -> r

Lysxia / Set.hs

Last active October 18, 2018 00:17

	{-# LANGUAGE FlexibleContexts, StandaloneDeriving, TypeFamilies, UndecidableInstances #-}

	module Set where

	import Data.List (nub)

	newtype Set0 s = Set0 { elems :: [Elt s] }

	deriving instance Eq (Elt s) => Eq (Set0 s)
	deriving instance Ord (Elt s) => Ord (Set0 s)

Lysxia / K.v

Last active October 25, 2018 02:15

	(* Some [IO] operations described by a sum type. *)
	Inductive IO : Type := I \| O (n : nat).

	(* A function computes the result type of every operation. *)
	Definition result : IO -> Type := fun io =>
	match io with
	\| I => nat
	\| O _ => unit
	end.

Lysxia / topo.v

Created October 29, 2018 13:45

	Require Export Ensembles.
	Arguments Full_set {U}.
	Arguments Empty_set {U}.
	Arguments In {U}.
	Arguments Intersection {U}.
	Arguments Union {U}.
	Arguments Complement {U}.

	Definition Family A := Ensemble (Ensemble A).
	Inductive FamilyUnion {T : Type} (F: Family T) : Ensemble T :=

Lysxia / W.v

Created October 30, 2018 18:24

	Require Import ZArith List String Omega.
	Require Import Paco.paco.
	Import ListNotations.

	Set Implicit Arguments.
	Set Contextual Implicit.


	CoInductive stream (A:Type) :=
	\| snil : stream A

Lysxia / Foo.hs

Created November 8, 2018 05:08

	import Control.Monad.Trans
	import Control.Monad.Trans.Cont

	bracket :: Monad m => ContT a m a -> ContT r m a
	bracket (ContT f) = ContT $ \k -> f pure >>= k

	defer :: Monad m => ContT () m () -> ContT r m ()
	defer (ContT f) = ContT $ \k -> k () <* f pure

	main :: IO ()

Lysxia / Test.hs

Created November 14, 2018 00:20