aljce

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

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

aljce

module Para where

open Agda.Primitive using (lsuc)

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

infixr 5 _∷_

aljce

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

aljce

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

aljce

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) →

aljce

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

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)

aljce

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

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