cheery

module Simple where

import Bwd -- https://gist.github.com/cheery/eb515304a0a7bcf524cb89ccf53266c2

data Interval
  = I0
  | I1
  | In Int
  deriving (Show, Eq)

cheery

module Bwd where

data Bwd a = Empty
           | Bwd a :> a

instance Functor Bwd where
  fmap f Empty = Empty
  fmap f (xs :> x) = fmap f xs :> f x

instance Eq a => Eq (Bwd a) where

cheery

module CatPu where

import Control.Applicative (Alternative (..))
import Control.Monad (MonadPlus (..), foldM, forM)
import Control.Monad.State
import Control.Monad.Except
import Data.List (intersect, elemIndex)

type Goal = SolverState -> Stream SolverState

cheery

{-# OPTIONS --cubical #-}
module hedberg where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws

data Empty : Set where

absurd : {A : Set} → Empty → A

cheery

module newtry6 where
-- derived from https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
--              http://eprints.nottingham.ac.uk/41385/1/th.pdf

open import Level
open import Function using (id; _∘_)

infixr 5 _⇒_

data Ty : Set where

cheery

module newtry where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Data.Fin
open import Data.Nat
open import Data.Product
open import Data.Empty

cheery

module demo where

open import Agda.Builtin.Equality
open import Data.List
open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Data.Fin.Base
open import Data.Product
open import Data.Sum

cheery

{-# OPTIONS --type-in-type #-}
module demo where

open import Data.Product
open import Data.Unit
open import Agda.Builtin.Equality

data Unit₁ : Set₁ where
    point : Unit₁

cheery

{-# OPTIONS --guardedness #-}
module demo where

open import Data.Product
open import Data.Empty
open import Agda.Builtin.Equality
open import Agda.Primitive

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

cheery

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs, FlexibleContexts #-}
module SimplyDifficult where

-- This thing demonstrates dynamic pattern unification,
-- however the examples are too simple to verify that the unifier is
-- working correctly.

-- There were also a thing or two that were way too hard to implement.
-- I've omitted them.