aljce

UB Midrange: 
You want to get to 5 mana asap so that you can start casting your 3 mana bangers through counter magic.
If you achieve this you win the game basically every time. Thran spider is the goat. 
We bring out our 5 mana spells as they get countered. Net comes out because often if net matters it will be tidebindered.
If you attempt to draw cards off the net you where probably gonna win that game anyway.
In:
  1 Elspeth's Smite
  3 Negate 
  2 Split Up
Out:

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
⊤ = ⊥ → ⊥