Skip to content

Instantly share code, notes, and snippets.

Xia Li-yao Lysxia

Block or report user

Report or block Lysxia

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
@Lysxia
Lysxia / reverse.v
Created Sep 14, 2019
Reverse lists in linear time with difference lists
View reverse.v
Require Import List.
Import ListNotations.
Fixpoint reverse {A} (xs : list A) : list A :=
match xs with
| [] => []
| x :: xs => reverse xs ++ [x]
end.
Module DList.
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;
View A.v
Goal (0 = 0 /\ 1 = 1).
Proof.
split.
all: reflexivity.
Qed.
Ltac foo := split.
Goal (0 = 0 /\ 1 = 1).
Proof.
View A.hs
{-# LANGUAGE KindSignatures #-}
module A where
class C (f :: * -> * -> *)
View a.hs
{-# LANGUAGE RankNTypes, DerivingStrategies, GeneralizedNewtypeDeriving #-}
-- Defaults to newtype
newtype T_Def = T_Def Bool
deriving (Eq, Ord, Bounded)
-- Stock
newtype T_S = T_S Bool
deriving stock (Eq, Ord, Bounded)
View viacodensity.hs
{-# Language KindSignatures, RankNTypes, DerivingVia #-}
newtype Foo i o m r = Foo (Await i m r -> Yield o m r -> m r)
newtype Pipe i o m a = Pipe (forall xx. (a -> Await i m xx -> Yield o m xx -> m xx) -> (Await i m xx -> Yield o m xx -> m xx))
deriving (Functor, Applicative, Monad)
via Codensity (Foo i o m)
-- Fluff --
View GHas.hs
data Path = L Path | R Path | Here
data MPath = NotFound | Conflict | Found Path
type family Search a (f :: k -> Type) :: MPath where
-- ...
Search a (f :*: g) = OrPath (Search a f) (Search a g)
Search a (K1 i c) = Check a c
type family Check a c where
View tcase.v
Require Import List Arith Ascii String Fin.
Require Import MetaCoq.Template.All.
Import ListNotations MonadNotation.
Set Universe Polymorphism.
Local Open Scope string_scope.
(* Get the [one_inductive_body] from a [mutual_inductive_body].
Fails if there is more than one. *)
Definition get_ind_body (tyDef : mutual_inductive_body)
View CatMonad.hs
{-# LANGUAGE GADTs, FunctionalDependencies, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
module CatMonad where
import Control.Category as C
import Data.Kind
class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where
type Id c :: c x x
type Cat c (f :: c x y) (g :: c y z) :: c x z
@Lysxia
Lysxia / CatMonad.hs
Last active Jul 15, 2019
Monads indexed by categories
View CatMonad.hs
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
module CatMonad where
import Control.Category as C
import Data.Kind
class CatMonad (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) where
type Id m :: c x x
type Cat m (f :: c x y) (g :: c y z) :: c x z
You can’t perform that action at this time.