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

# -*- encoding: utf-8 -*-
# Implements symmetric interaction combinators
# I took some ideas from Victor Maia's projects. 

# Bunch of cells form an interaction net.
# It's a half-edge graph.
class Cell:
    def __init__(self, kind):
        self.ports = (Port(self), Port(self), Port(self))
        self.kind = kind # 'era', 'con', 'fan'

cheery

#!/usr/bin/env python
"""
    Run programs with added vulkan layers.
    
    Author: Henri Tuhola <henri.tuhola@gmail.com>
    License: MIT
    Date: 2016-2-20
"""
import argparse, json, os, sys

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

def state_0(ch):
    if ch == None:
        return None
    if ch == "1":
        return state_4
    if ch == 'int':
        return state_1
    if ch == 'plus':
        return state_1
    assert False