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.

cheery

module SimplyEasy where
-- From the paper: http://strictlypositive.org/Easy.pdf
-- An attempt to add case -statement.
-- Fails on typechecking a case.

data Name
    = Const String
    | Bound Int
    | Unquoted Int
    deriving (Show, Eq)

cheery

from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core

class SThread(StackletThread):
    def __init__(self, config):
        StackletThread.__init__(self, config)
        self.cont = None

def get_sthread():

cheery

# -*- encoding: utf-8 -*-
class TermOrVar(object):
    def to_str(self, rbp=0):
        assert False

class Term(TermOrVar):
    def __init__(self, name, args):
        self.name = name
        self.args = args
        for arg in args:

cheery

module lam where

open import Data.List
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Data.Sum

data Ty : Set where
  _⊗_ : Ty → Ty → Ty

cheery

from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core

class SThread(StackletThread):
    def __init__(self, config):
        StackletThread.__init__(self, config)
        self.cont = None

def get_sthread():

cheery

module Regex2 where

open import Function
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.List as List
open import Data.Empty
open import Data.Unit

cheery

module FinMap where

open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality using (refl; cong; trans; subst; sym)
open import Data.Nat as ℕ using (ℕ; _<_; _≤_; suc; s≤s; z≤n)
open import Data.Nat.Properties using (≤-refl; +-comm; +-identityˡ; +-identityʳ; +-suc; 1+n≢0)
open import Data.Fin hiding (compare; _<_; _≤_)
open import Data.List
open import Data.Product
open import Data.Sum

cheery

module parsergen4 where

-- for troubleshooting, not a complete parser generator/parsing engine.

open import Agda.Builtin.Equality
open import Relation.Nullary using (Dec)
open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.Fin.Properties using (suc-injective)
open import Data.Vec hiding (_>>=_)