Skip to content

Instantly share code, notes, and snippets.

View aljce's full-sized avatar

Alice McKean aljce

  • Portland, OR
View GitHub Profile
runWithAsaModes
:: ( AsaMode
-> ( String
-> YT.SIO (YT.YesodExampleData App) (AsaTestState Identity)
-> SpecWith (Arg (YT.SIO (YT.YesodExampleData App) (AsaTestState Identity)))
)
-> SpecWith (Arg (YT.SIO (YT.YesodExampleData App) ()))
)
-> SpecWith (Arg (YT.SIO (YT.YesodExampleData App) ()))
runWithAsaModes cb = do
@aljce
aljce / ChurchList.agda
Last active March 21, 2023 23:28
GPT4 ChurchList conversion
-- Prompt: can you prove that churchlists are isomorphic to regular lists in agda
-- Define natural numbers
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
-- Define regular lists
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
module Para where
open Agda.Primitive using (lsuc)
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
infixr 5 _∷_
import Control.Exception (finally)
import Control.Concurrent.STM (atomically)
import Control.Concurrent.STM.TMVar (TMVar, newEmptyTMVarIO, takeTMVar, putTMVar, readTMVar)
prerun :: (IO a -> IO (IO b)) -> IO (IO a -> IO b)
prerun f = do
mailbox <- newEmptyTMVarIO
-- mailbox for actions (IO a)
mb <- f (join (atomically (readTMVar mailbox)))
-- run the action inside the mailbox up to n times
data Extension a = Extension
{ real :: !a, extn :: !a } -- real + extn*sqrt(5)
deriving Show
instance Num a => Num (Extension a) where
(Extension a b) + (Extension c d) = Extension (a + c) (b + d)
(Extension a b) - (Extension c d) = Extension (a - c) (b - d)
(Extension a b) * (Extension c d) = Extension (a * c + 5 * b * d) (a * d + b * c)
negate (Extension a b) = Extension (negate a) (negate b)
fromInteger n = Extension (fromInteger n) 0
let Map = http://prelude.dhall-lang.org/Map/Type
let Entry = http://prelude.dhall-lang.org/Map/Entry
let map = http://prelude.dhall-lang.org/Map/map
let TerraformType
: Type
= ∀(type : Type) →
∀(TerraformString : type) →
∀(TerraformNumber : type) →
∀(TerraformBool : type) →
∀(TerraformList : type → type) →
import math
import cmath
tau = 2 * cmath.pi
def wave(n, f):
res = []
j = 0
while (j < n):
res.append(math.sin(tau * f * j))
@aljce
aljce / Divisiblity.agda
Last active January 10, 2020 21:12
Semiring polymorphic gcd + bezouts lemma
open import Level using (_⊔_)
open import Function using (_$_)
open import Data.Empty using (⊥)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Rel; Reflexive; Transitive; Antisymmetric; _Respects₂_; _Respectsʳ_; _Respectsˡ_; Symmetric; Decidable; Irrelevant)
open import Relation.Binary.PropositionalEquality using (_≡_) renaming (refl to ≡-refl; cong to ≡-cong)
{-# OPTIONS --prop --type-in-type #-}
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
module False (extensionality : ∀ (A B : Prop) → A ≡ B) where
⊥ : Prop
⊥ = ∀ (p : Prop) → p
⊤ : Prop
⊤ = ⊥ → ⊥
@aljce
aljce / shell.nix
Created September 8, 2019 01:40
A reproducible rust build environment
# A fully reproducible rust build environment via nix
# run `nix-shell` to enter the build enviroment
# run `nix-shell --argstr backtrace true` to enable backtracing
with rec {
fetch-github =
{ owner # The owner of the repo
, repo # The repo to fetch
, rev # The git commit hash you want
, sha256 # The SHA256 hash of the unpacked archive (for reproducibility)
}: builtins.fetchTarball {