prozacchiwawa

Keybase proof

I hereby claim:

• I am prozacchiwawa on github.
• I am arty (https://keybase.io/arty) on keybase.
• I have a public key ASBOAvnkixLoUYOuqvhsBNHwYj_vltAecfEJ9JdgC7nH5Qo

To claim this, I am signing this object:

prozacchiwawa

import Decidable.Equality

data RETree : (t : Type) -> Type where
  End : RETree t
  Item : t -> RETree t
  Sequence : RETree t -> RETree t -> RETree t
  OneOrTheOther : RETree t -> RETree t -> RETree t
  Repeated : RETree t -> RETree t -> RETree t

simpleItemAppliesToRE : (DecEq t) => t -> t -> Bool

prozacchiwawa

def mini_parse_schema(lines):
    have_tables = {}
    for line in lines:
        first_paren_idx = line.index('(')
        if first_paren_idx == -1:
            continue

        end_paren_idx = line.rindex(')')
        if end_paren_idx == -1:
            continue

prozacchiwawa

#!/usr/bin/env python
import sys
import sqlite3

COPY_BLOCKS=1000
block_records_fields = [
       'header_hash',
       'prev_hash',
       'height',
       'weight',

prozacchiwawa

module F1

import System
import Data.Bool
import Data.List
import Data.Vect
import Decidable.Equality

data Fruit = Apple | Banana

prozacchiwawa

module DecBool

-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
  where
    fEf : False = False
    fEf = Refl

prozacchiwawa

import xml.dom.minidom
import sys

def traverse(e,o):
    oldwhere = None
    useo = dict(o.items())

    if e.nodeType == e.TEXT_NODE:
        return

prozacchiwawa

;;; mood-dark-theme.el - Coding palette based on atari 2600 colors. based on the following
;; emacs theme:

;; spacemax-common.el --- Color theme with a dark and light versions.

;; Copyright (C) 2019 Michael Camilleri

;; Author: Michael Camilleri
;; URL: <https://github.com/pyrmont/spacemax-theme>
;;

prozacchiwawa

import sys

def shiftout(fout, bs):
    for b in bs:
        bb = b
        for i in range(8):
            if (bb >> 7) % 2 == 0:
                fout.write(bytes([255]))
            else:
                fout.write(bytes([0]))

prozacchiwawa

data SignedNat : Bool -> Nat -> Type where
  Neg : (n:Nat) -> SignedNat True n
  Pos : (n:Nat) -> SignedNat False n

data Memory : sna -> mem -> Type where
  MWord : sna -> mem -> Memory sna mem
  MEnd : sna -> Memory sna Void

data MemoryAddress : Nat -> Type where
  MAddr : (n:Nat) -> MemoryAddress n