ckoparkar

module Tree where

data Tree = Leaf Int | Node Int Tree Tree
  deriving (Show, Read, Eq, Ord)

type Forest = [Tree]

mkTree :: Int -> Tree
mkTree n =
  case n of

ckoparkar

;; depends on monger
;; [com.novemberain/monger "3.1.0"]

(ns cider.nrepl.middleware.see-also
  (:require [monger.core :as mg]
            [monger.collection :as c]))

(defn extract-see-alsos
  []
  (let [conn (mg/connect)

ckoparkar

To get around this, we have to prove that this recursion is "welll-founded". Consider the example of `<` and `<=`. The 
relation `<` is well-founded but `<=` is not. Because in `a < b < c`, we know that `a` is strictly less than `b`. This is 
finite and terminating. Whereas we can make infinite chains of `a <= a <= a ...`. This is called "accessibility". Using this 
concept, we have to prove that our `power` function is well-founded. I cannot fully explain this here; I am still working on 
understanding it completely. But this talk by Eric Mertens, https://vimeo.com/36519234 is really great. And here's a similar 
implementation in Idris, https://github.com/idris-lang/Idris dev/blob/0d3d2d66796b172e9933360aee51993a4abc624d/libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr.

ckoparkar

(define unops '(sub1 zero? car cdr))
(define binops '(* + > >= < <= = cons))

(define empty-env
  (lambda ()
    '(empty-env)))

(define extend-env
  (lambda (var val env)
    `(extend-env ,var ,val ,env)))

ckoparkar

data Parity : ℕ -> Set where
  even : (k : ℕ) -> Parity (k * 2)
  odd  : (k : ℕ) -> Parity (1 + k * 2)

parity : (n : ℕ) -> Parity n
parity zero = even zero
parity (succ n) with parity n
parity (succ .(k * 2)) | even k = odd k
parity (succ .(1 + k * 2)) | odd k = even (succ k)

ckoparkar

 Elaborating Main.SplitView
 Cryptol.idr:83:6
 Main.SplitView pre-type {n : Nat} ->
(m : Nat) ->
Vect (mult m
n)
a ->
Type[]
 Main.SplitView type []
{a : _} ->

ckoparkar

{-----------------------------------------------------------------

A "Tree" represents a binary tree. A "Node" in a binary tree
always has two children. A tree can also be "Empty". Below I have
defined "Tree" and a number of useful functions.

This example also includes some challenge problems :)

-----------------------------------------------------------------}

ckoparkar

1. Install nightly build of cargo. (rustfmt requires cargo 0.6.0 or newer)

   $ curl -sSf https://static.rust-lang.org/rustup.sh | sh -s -- --channel=nightly

2. Then install rustfmt,

   $ cargo install --git https://github.com/rust-lang-nursery/rustfmt

3. Install emacs-rustfmt

ckoparkar

{
    "bootstrap": true,
    "server": true,
    "datacenter": "con",
    "data_dir": "/tmp/consul",
    "encrypt": "yJqVBxe12ZfE3z+4QSk8qA==",
    "log_level": "INFO",
    "enable_syslog": true,
    "ui_dir": "~/consul_config/dist",
    "acl_datacenter": "con",

ckoparkar

#!/usr/bin/env bash
# Save and restore the state of tmux sessions and windows.
# TODO: persist and restore the state & position of panes.
set -e

dump() {
  local d=$'\t'
  tmux list-windows -a -F "#S${d}#W${d}#{pane_current_path}"
}