cheery

# Please note that this thing is not complete and grifters will adjust to it.
# I update this from time to time.
# 29.11.2024
# At the moment this script is not a turnkey solution,
# also you're meant to read it through before running it!

"""
Copyright 2024 Henri Tuhola

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

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

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