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

function main() {
    interaction_example();
    arithmetic_example();
}

function interaction_example() {
    var plug = make_terminal_plug();

    var code = [
        SEL, 1,

cheery

is_carnivore_in_1971 = {}
is_alive_in_1992 = {}
age_of_death = {}

with open('nhanes/DU4701.txt', 'r') as fd:
    rows = fd.readlines()
    for row in rows:
        sample = row[0:5]
        meat_freq = int(row[224:228])
        diet = [0, 0, 0]

cheery

module Structures where

open import Data.Unit
open import Data.Product
open import Data.Empty
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Maybe
open import Data.List

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

# -*- 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