louisswarren

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)

record Σ (I : Set)(I→S : I → Set) : Set where
  constructor _,_
  field
    fst : I
    snd : I→S fst

-- Partition members of A by their values of f

louisswarren

# Display a note if the kernel has been updated

import re
import subprocess

def run(*cmdlist):
    return subprocess.run(cmdlist, stdout=subprocess.PIPE).stdout.decode()

def running_version():
    uname_result = run('uname', '-r')

louisswarren

# py3status module for playerctl

import subprocess

def run(*cmdlist):
    return subprocess.run(
            cmdlist,
            stdout=subprocess.PIPE,
            stderr=subprocess.DEVNULL).stdout.decode()

louisswarren

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

data Bool : Set where
  true  : Bool
  false : Bool

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

louisswarren

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

record ⊤ : Set where
data ⊥ : Set where

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

louisswarren

class Foo:
    def __init__(self, name):
        self.name = name

    def __eq__(self, other):
        print("Testing if {} == {}".format(self.name, other.name))
        return True

    def __str__(self):
        return self.name

louisswarren

data Bool : Set where
  true  : Bool
  false : Bool


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

louisswarren

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n = n
(suc n) + m = suc (n + m)

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

louisswarren

sample = '''
5 3
1 4 10 1 1
1 1 8 1 1
1 1 9 1 1
'''

def best_profit(prices, cpus_left, profit=0):
    if not prices:
        return profit

louisswarren

(add-pvar-name "P" "Q" (make-arity))

(define (mk-disj phi psi)
  (mk-imp
    (mk-imp phi (pf "Pvar"))
    (mk-imp
      (mk-imp psi (pf "Pvar"))
      (pf "Pvar"))))

(define (mk-neg phi) (mk-imp phi (pf "bot")))