luxbock

  ;; Expanding the following expression as far as it can go:

  (filter even? (range 10))

  ;; equals

  (lazy-seq
    (when-let [s (seq (range 10))]
      (if (chunked-seq? s)
        (let [c (chunk-first s), size (count c), b (chunk-buffer size)]

luxbock

(transform
  [MAP-VALS
   (view frequencies)
   (collect-one (view #(apply max (vals %))))]
  (fn [mx fs] (transform MAP-VALS #(/ % mx) fs))
  {:a [1 1 3 4] :b [1 1 2 2 2 3]})

;; => {:a {1 1, 3 1/2, 4 1/2}, :b {1 2/3, 2 1, 3 1/3}}

luxbock

(ns test.core
  (:require [clojure.spec :as s]
            [clojure.spec.test :as stest]
            [clojure.test.check.generators :as gen]))

(s/def ::file-count nat-int?)
(s/def ::operations (s/map-of keyword? pos-int?))
(s/def ::time-total (s/and double? (complement neg?)))

(s/def ::summary-res

luxbock

(defn- get-fspec-attr
  [sym attr]
  (->> (s/form sym)
       (rest)
       (partition 2)
       (keep (fn [[a b]] (when (= a attr) b)))
       (first)))

(s/fdef conform-fn-call
  :args (s/cat :fn-call (s/spec (s/cat :f symbol? :rs (s/* any?))))

luxbock

(defnav take-nth [n]
  (select* [this structure next-fn]
    (next-fn (take-nth n structure)))
  (transform* [this structure next-fn]
    (if (vector? structure)
      (let [c  (count structure)
            is (into []
                 (take-while #(< % c))
                 (iterate #(+ % n) 0))]

luxbock

(defnav drop-nav [n]
  (select* [this structure next-fn]
    (next-fn
      (if (vector? structure)
        (subvec structure (min n (count structure)))
        (drop n structure))))
  (transform* [this structure next-fn]
    (if (vector? structure)
      (let [mi (min n (count structure))]
        (into (subvec structure 0 mi)

luxbock

(defnav every-nth [n]
  (select* [this structure next-fn]
    (next-fn (take-nth n structure)))
  (transform* [this structure next-fn]
    (let [xform (comp
                  (map-indexed
                    (fn [i x]
                      (if (zero? (mod i n))
                        (next-fn x)
                        x)))

luxbock

/// Santa is delivering presents to an infinite two-dimensional grid of houses.
///
/// He begins by delivering a present to the house at his starting location, and then an elf at the North Pole calls him via radio and tells him where to move next. Moves are always exactly one house to the north (^), south (v), east (>), or west (<). After each move, he delivers another present to the house at his new location.
///
/// However, the elf back at the north pole has had a little too much eggnog, and so his directions are a little off, and Santa ends up visiting some houses more than once. How many houses receive at least one present?
///
/// For example:
///
/// > delivers presents to 2 houses: one at the starting location, and one to the east.
/// ^>v< delivers presents to 4 houses in a square, including twice to the house at his starting/ending location.

luxbock

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := 
iff.intro
  (assume h, _)
  /-
  propositions_as_types.lean:432:13: error 
  don't know how to synthesize placeholder
  context:
  p q r : Prop,
  h : p ∨ q → r
  ⊢ (p → r) ∧ (q → r)

luxbock

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (assume h : p ∧ (q ∨ r),
    have hp : p, from h.left,
    or.elim h.right
      (assume hq, or.inl ⟨hp, hq⟩)
      (assume hr, or.inr ⟨hp, hr⟩))
  (assume h : (p ∧ q) ∨ (p ∧ r),
    or.elim h
      (assume hpq,