Skip to content

Instantly share code, notes, and snippets.

luxbock luxbock

Block or report user

Report or block luxbock

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View prime_eval.lean
namespace hidden
open classical
open decidable
local attribute [instance] prop_decidable
def divides (m n : ℕ) : Prop := ∃ k, m * k = n
instance : has_dvd ℕ := ⟨divides⟩
View halp.lean
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,
View inference_fail.lean
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,
View lean_hmm.lean
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)
View aoc-day3.rs
/// 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.
View every-nth.clj
(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)))
View navs.clj
(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)
View take-nth.clj
(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
luxbock / conform-fn-call.clj
Created Jan 27, 2017
Handy helper for when it comes to playing around with :fn predicates at the REPL
View conform-fn-call.clj
(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
luxbock / core.clj
Created Jan 24, 2017
Instrumenting generators trouble
View core.clj
(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
You can’t perform that action at this time.