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.

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