Isweet

Keybase proof

I hereby claim:

• I am isweet on github.
• I am iannsweet (https://keybase.io/iannsweet) on keybase.
• I have a public key ASBYgvgQeXgcKoIT3UpwncW20GyjhHgd0qSr9dwzOQNONQo

To claim this, I am signing this object:

Isweet

Election in Wysteria

Attempt 1

The most natural way to try express the elect function in Wysteria is using its support for first-class party sets.

let elect (parties : ps{true}) (n : nat) : ps{subeq parties} = ??

Isweet

// dep.h
int dep();

// dep.c 
#include "dep.h"

int dep() {
  return 10;
}

Isweet

import sys
from PIL import Image
from PIL import ImageFont
from PIL import ImageDraw
import qrcode

def concat_vertical(image1, image2):
    w1, h1 = image1.size
    w2, h2 = image2.size
    w = max(w1, w2)

Isweet

Inductive ev_dumb : nat -> Prop :=
  | EvDBase : ev_dumb 0
  | EvDRec  : forall n, ev_dumb n /\ n <> 1 -> ev_dumb (S (S n)).

Check ev_dumb_ind.

(* ev_dumb_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, ev_dumb n /\ n <> 1 -> P (S (S n))) -> forall n : nat, ev_dumb n -> P n
*)

Isweet

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS : forall n, ev n -> ev (S (S n)).

Hint Constructors ev.

Inductive test : (nat -> nat) -> nat -> Prop :=
  | TestCase : forall f i,
      (forall k,
        0 <= k < f i ->

Isweet

Inductive ev_dumb : nat -> Prop :=
  | EvDBase : ev_dumb 0
  | EvDRec  : forall n, ev_dumb n /\ n <> 1 -> ev_dumb (S (S n)).

Check ev_dumb_ind.

(* ev_dumb_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, ev_dumb n /\ n <> 1 -> P (S (S n))) -> forall n : nat, ev_dumb n -> P n
*)

Isweet

Require Import Coq.Logic.ClassicalChoice.

Definition two (n : nat) : Prop := n = 0 \/ n = 1.

Lemma zero_in_two : two 0.
Proof.
  unfold two. left. reflexivity.
Qed.

Lemma one_in_two : two 1.

Isweet

import qualified Data.Set as Set
import qualified Data.Array.IArray as Array

type Var = String
type Lab = Integer

type RD = Set.Set (Var, Lab)

type VecRD = Array.Array Integer RD
type VecF = Array.Array Integer (Solution -> RD)

Isweet

#! /bin/bash

cat << EOF > ./RandAscii.hs
module Main (main) where

import Control.Monad

import System.Random
import qualified Data.Char as Char