RyanGlScott’s gists

RyanGlScott / cabal.project.local

Last active September 30, 2023 23:53

GHC 9.8 cabal.project.local

RyanGlScott / SimplifiedExample.v

Last active November 22, 2022 20:30

	From Coq Require Import Program.Basics.
	From Coq Require Program.Equality.
	From Coq Require Import Vectors.Vector.
	From Coq Require Import Logic.Eqdep.

	Import VectorNotations.

	Require Import Lia.
	Require Import ZArith.
	Require Import ZifyBool.

RyanGlScott / ZifyTermTakeOne.v

Created November 21, 2022 14:48

A failing attempt to use https://github.com/coq/coq/pull/16868

	From Coq Require Import Program.Basics.
	From Coq Require Program.Equality.
	From Coq Require Import Vectors.Vector.
	From Coq Require Import Logic.Eqdep.

	Import VectorNotations.

	Require Import Lia.
	Require Import ZArith.
	Require Import ZifyBool.

RyanGlScott / HDList.hs

Created July 23, 2022 20:10

Heterogeneous difference lists

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE StandaloneKindSignatures #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}
	module HDList where

	import qualified Control.Category as Cat (Category(..))
	import Data.Function (on)

RyanGlScott / DList.v

Last active July 24, 2022 12:33

Proofs of the difference list invariant for various operations

	Require Import Lists.List.
	Import ListNotations.
	Open Scope list_scope.
	Require Import Logic.FunctionalExtensionality.
	Require Import Lists.Streams.

	Inductive DList (a : Type) : Type :=
	\| MkDList : (list a -> list a) -> DList a.
	Arguments MkDList {a} f.

RyanGlScott / FromToVec.hs

Created August 28, 2021 15:00

Proofs involving conversion from and to length-indexed vectors

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE StandaloneKindSignatures #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	module FromToVec where

RyanGlScott / Main.hs

Last active May 19, 2021 13:46

Is this use of unsafeCoerce valid?

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE NoStarIsType #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE TypeOperators #-}
	{-# OPTIONS_GHC -Wall #-}
	module Main (main) where

RyanGlScott / TakesForeverToCompile.hs

Created July 21, 2019 20:56

Try compiling with -O1 if you have a lot of time on your hands

	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeInType #-}
	{-# LANGUAGE TypeOperators #-}

RyanGlScott / ThePowerOfDefun.hs

Created July 20, 2019 12:46

	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}
	-- Requires GHC 8.10 or later
	module ThePowerOfDefun where

RyanGlScott / SingletonsVTA.hs

Created May 31, 2019 15:37

A sketch of how we might single visible type applications

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TopLevelKindSignatures #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}

Ryan Scott RyanGlScott