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
(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?)))) |
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
(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))] |
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
(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))) |
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
/// 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. |
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
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) |
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
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, |
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
open classical | |
variables (α : Type) (p q : α → Prop) | |
variable r : Prop | |
variable a : α | |
example : (∃ x, p x → r) ↔ (∀ x, p x) → r := | |
iff.intro | |
(assume ⟨a, pair⟩, | |
assume h : ∀ x, p x, |
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
namespace hidden | |
open classical | |
open decidable | |
local attribute [instance] prop_decidable | |
def divides (m n : ℕ) : Prop := ∃ k, m * k = n | |
instance : has_dvd ℕ := ⟨divides⟩ |
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
(defn breadth-first-search [z] | |
(letfn [(zip-children [loc] | |
(when-let [first-child (zip/down loc)] | |
(take-while (comp not nil?) | |
(iterate zip/right first-child))))]) | |
(loop [ret [] | |
queue (conj clojure.lang.PersistentQueue/EMPTY z)] | |
(if (seq queue) | |
(let [[node children] ((juxt zip/node zip-children) (peek queue))] | |
(recur (conj ret node) (into (pop queue) children))) |