| (defn heredoc [] | |
| (let [delim (.readLine *in*)] | |
| (->> (repeatedly #(.readLine *in*)) | |
| (take-while #(not= delim %)) | |
| (interpose \newline) | |
| (apply str)))) | |
| ; The following lines are read (by the reader) as: | |
| ; "Look )(\"\\T\na here doc!\n" | |
| #=(heredoc)""" |
| Require Import Coq.Setoids.Setoid. | |
| Require Import Arith. | |
| Notation "`Begin p" := p (at level 20, right associativity). | |
| Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity). | |
| Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity). | |
| Notation "a `End" := (@eq_refl _ a) (at level 10). | |
| Definition times2 : forall n, n + n = 2 * n := fun n => | |
| `Begin |
| {-# LANGUAGE ExistentialQuantification, RankNTypes #-} | |
| {- | |
| Monadic generation and simplification of examples | |
| It's easy to generate data monadically (that's just a Random monad) but it's | |
| less obvious how to proceed in a way that allows you to simplify the generated | |
| data. It's not even obvious how to do it functorially. |
| #!/bin/bash | |
| # Intearctively select one of the recent branches and checkout it. | |
| set -e | |
| git rev-parse --is-inside-work-tree >/dev/null | |
| git checkout $(git for-each-ref --sort=-committerdate --format='%(refname:short)' refs/heads/ | fzf -q "$*") |
| (* How do to topology in Coq if you are secretly an HOL fan. | |
| We will not use type classes or canonical structures because they | |
| count as "advanced" technology. But we will use notations. | |
| *) | |
| (* We think of subsets as propositional functions. | |
| Thus, if [A] is a type [x : A] and [U] is a subset of [A], | |
| [U x] means "[x] is an element of [U]". | |
| *) | |
| Definition P (A : Type) := A -> Prop. |
| (defproject parser-vuln-test "1.0" :dependencies [[org.clojure/clojure "1.6.0"]]) |
Usage
osascript Start.applescript "objective" "tag1,tag2"
osascript Stop.applescript
I have skipped most Vitamin-R workflows. See the attached settings snapshot. If you have them enabled, you need to update the script to handle different steps.
I use the scripts in my org pomodoro script
A lot of math grad school is reading books and papers and trying to understand what's going on. The difficulty is that reading math is not like reading a mystery thriller, and it's not even like reading a history book or a New York Times article.
The main issue is that, by the time you get to the frontiers of math, the words to describe the concepts don't really exist yet. Communicating these ideas is a bit like trying to explain a vacuum cleaner to someone who has never seen one, except you're only allowed to use words that are four letters long or shorter.
What can you say?
All links are amazon affiliate. I'm recommending you books, it's how I pay to buy my own. ;)
FWIW, here are a few common answers to clear your worries about parentheses in Clojure in particular:
It's idiomatic to use indentation to display what's nested within a given set of parentheses. The preferred way to indent code is documented fairly well. [Edit: A few examples are found e.g. here: http://clojure-euler.wikispaces.com/Problem+001]
If you're concerned about matching parens somewhere (i.e. you suspect things aren't correctly indented), use your text editor to blink the matching bracket and fix the indents if needed.
Typical function definitions in Clojure are somewhere between 1 and 20 lines — there's isn't much to match. In case you have more, break things to new functions (or more likely, use the core library functions better to your advantage).