This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Simple where | |
import Bwd -- https://gist.github.com/cheery/eb515304a0a7bcf524cb89ccf53266c2 | |
data Interval | |
= I0 | |
| I1 | |
| In Int | |
deriving (Show, Eq) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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₁ |
NewerOlder