thomasdziedzic

Require Import Coq.PArith.BinPos.
Require Import Coq.NArith.BinNat.

Open Scope positive_scope.
Open Scope N_scope.

Fixpoint chomp10s (p : positive) : N :=
  match p with
  | p'~1~0 => chomp10s p'
  | 1~0 => N0

thomasdziedzic

module Exercises.My

import Data.Vect

%default total

public export
data CFT : Nat -> Type where
  Var   : Fin n -> CFT n
  Zero  : CFT n

thomasdziedzic

import org.apache.spark.streaming._
import org.apache.spark.streaming.kafka010._
val kafkaParams = Map("metadata.broker.list" -> "localhost:9092")
val topics = Set("test")
val streamingContext = new StreamingContext(sc, Seconds(1))
val kafkaStream = KafkaUtils.createDirectStream(streamingContext, kafkaParams, topics)
kafkaStream.print()
streamingContext.start()

thomasdziedzic

   0xb7f36b2f <+1302>:  mov    esi,0x5
   0xb7f36b34 <+1307>:  xor    ebx,ebx
=> 0xb7f36b36 <+1309>:  mov    eax,DWORD PTR [ebx+0x1c0]

thomasdziedzic

==> Starting package_ruby-gtk2()...
(cd ext/gtk2 && make install)
make[1]: Entering directory `/build/src/ruby-gtk2-1.2.1/gtk2/ext/gtk2'
/usr/bin/install -c -m 644 /build/src/ruby-gtk2-1.2.1/gtk2/ext/gtk2/rbgdk.h /build/pkg/ruby-gtk2//usr/lib/ruby/vendor_ruby/2.0.0/x86_64-linux
/usr/bin/install: cannot overwrite directory '/build/pkg/ruby-gtk2//usr/lib/ruby/vendor_ruby/2.0.0/x86_64-linux' with non-directory
make[1]: *** [install-headers] Error 1
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory `/build/src/ruby-gtk2-1.2.1/gtk2/ext/gtk2'
make: *** [install] Error 2
==> ERROR: A failure occurred in package_ruby-gtk2().

thomasdziedzic

<?xml version="1.0" encoding="UTF-8"?>
<Profile xmlns="http://soap.sforce.com/2006/04/metadata">
    <classAccesses>
        <apexClass>AccountConferenceButtonControllerExt</apexClass>
        <enabled>false</enabled>
    </classAccesses>
    <classAccesses>
        <apexClass>AccountConferenceButtonControllerExtTest</apexClass>
        <enabled>false</enabled>
    </classAccesses>

thomasdziedzic

module Tree

{-
background/why

goals:
    1. Given a tree, flip it horizontally
    2. prove flip (flip t) = t
        i.e. flip is its own inverse or that flip is an involution

thomasdziedzic

module Tree

%default total

data Tree : Type -> Type where
  Leaf : Tree a
  Branch : (ltree : Tree a) -> a -> (rtree : Tree a) -> Tree a

flip : Tree a -> Tree a
flip Leaf = Leaf

thomasdziedzic

[22] pry(main)> work_items.all
=> [{"_id"=>BSON::ObjectId('50c015a96740747127000011'),
  "who"=>"asdf",
  "goal"=>"Looking for work",
  "description"=>"asdf"},
 {"_id"=>BSON::ObjectId('50c015c36740747127000012'),
  "who"=>"asdf",
  "goal"=>"Looking for work",
  "description"=>"asdf"}]
[23] pry(main)> work_items.remove '_id' => '50c015a96740747127000011'

thomasdziedzic

import Data.Vect

create_empties : Vect n (Vect 0 elem)
create_empties = replicate _ []

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = let xs_trans = transpose_mat xs in
                              zipWith (::) x xs_trans