This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Exercises.My | |
import Data.Vect | |
%default total | |
public export | |
data CFT : Nat -> Type where | |
Var : Fin n -> CFT n | |
Zero : CFT n |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/sh | |
set -e | |
YCM_DIR="${HOME}/.vim/bundle/YouCompleteMe" | |
YCM_GIT="https://github.com/Valloric/YouCompleteMe" | |
rm -rf "${YCM_DIR}" | |
git clone "${YCM_GIT}" "${YCM_DIR}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from faker import Factory | |
from datetime import datetime | |
import mysql.connector | |
import sys | |
def insertBatch(cnx, cursor, count): | |
fake = Factory.create() | |
data = [] | |
current_time = datetime.now() | |
for i in range(count): |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[root@anvl ~]# dmesg | grep -i mmc | |
[ 0.000000] Kernel command line: console=ttyO2,115200n8 mpurate=800 root=/dev/mmcblk0p2 rw rootfstype=ext4 rootwait | |
[ 0.967285] pbias_mmc_omap2430: 1800 <--> 3000 mV at 3000 mV | |
[ 2.054473] VMMC1: 1850 <--> 3150 mV at 3150 mV | |
[ 2.063507] VMMC2: 1850 <--> 3150 mV at 2600 mV | |
[ 2.896728] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@4809c000[0]' | |
[ 2.896759] of_get_named_gpiod_flags: can't parse 'wp-gpios' property of node '/ocp/mmc@4809c000[0]' | |
[ 2.949310] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@480b4000[0]' | |
[ 2.949340] of_get_named_gpiod_flags: can't parse 'wp-gpios' property of node '/ocp/mmc@480b4000[0]' | |
[ 2.989410] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@480ad000[0]' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[root@anvl ~]# dmesg | grep mmc | |
[ 0.000000] Kernel command line: console=ttyO2,115200n8 mpurate=800 root=/dev/mmcblk0p2 rw rootfstype=ext4 rootwait | |
[ 0.967285] pbias_mmc_omap2430: 1800 <--> 3000 mV at 3000 mV | |
[ 2.896728] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@4809c000[0]' | |
[ 2.896759] of_get_named_gpiod_flags: can't parse 'wp-gpios' property of node '/ocp/mmc@4809c000[0]' | |
[ 2.949310] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@480b4000[0]' | |
[ 2.949340] of_get_named_gpiod_flags: can't parse 'wp-gpios' property of node '/ocp/mmc@480b4000[0]' | |
[ 2.989410] of_get_named_gpiod_flags: can't parse 'cd-gpios' property of node '/ocp/mmc@480ad000[0]' | |
[ 2.989440] of_get_named_gpiod_flags: can't parse 'wp-gpios' property of node '/ocp/mmc@480ad000[0]' | |
[ 3.055114] mmc1: BKOPS_EN bit is not set |
NewerOlder