solson

module Posits
export Posit8, Posit16, Posit32, Posit64, Posit128, AbstractPosit

abstract type AbstractPosit{N, ES} <: Real end

for size in [8, 16, 32, 64, 128]
    Posit = Symbol("Posit", size)
    UInt = Symbol("UInt", size)

    @eval begin

solson

module FnMacro
export @fn

arg_name(n::Int) = Symbol("hole_", n)

rewrite(x,         n::Ref{Int}) = x
rewrite(s::Symbol, n::Ref{Int}) = s == :_ ? arg_name(n[] += 1) : s
rewrite(e::Expr,   n::Ref{Int}) = Expr(e.head, map(a -> rewrite(a, n), e.args)...)

macro fn(e)

solson

module What
export Whatever, what

struct Whatever{NumArgs, F <: Function}
    f::F
    Whatever{N}(f::F) where {N, F <: Function} = new{N, F}(f)
end

const what = Whatever{1}(identity)

solson

@[simp] theorem card_prod : card (α × β) = card α * card β := by simp [fintype.values] 
@[simp] theorem card_sum : card (α ⊕ β) = card α + card β := by simp [fintype.values] 
@[simp] theorem card_empty_prod : card (empty × α) = 0 := by simp [fintype.values] 
@[simp] theorem card_prod_empty : card (α × empty) = 0 := by simp [fintype.values] 
@[simp] theorem card_empty_sum : card (empty ⊕ α) = card α := by simp [fintype.values] 
@[simp] theorem card_sum_empty : card (α ⊕ empty) = card α := by simp [fintype.values] 
@[simp] theorem card_unit_prod : card (unit × α) = card α := by simp [fintype.values] 
@[simp] theorem card_prod_unit : card (α × unit) = card α := by simp [fintype.values] 
@[simp] theorem card_option : card (option α) = 1 + card α := by simp [fintype.values] 
theorem card_sum_eq_card_prod : card (α ⊕ α) = card (bool × α) := by simp [card, fintype.values]

solson

-- TODO(solson): lean/library/init/data/sum/default.lean should include this import upstream.
import init.data.sum.instances

universes u v

variables {α : Type u} {β : Type v} {n : ℕ} {a : α} {b : β} {f : α → β}

def count_cond [decidable_eq α] (a b : α) : ℕ :=
    cond (a = b) 1 0

solson

-- lemma mem_range_of_lt {x n : ℕ} : x < n → x ∈ range n :=
-- begin
--     assume h_lt,
--     induction n,
--     case nat.zero {
--         exfalso,
--         exact (nat.not_lt_zero x) h_lt,
--     },
--     case nat.succ n' ih_n {
--         rewrite range_step,

solson

-- def concat (L1 L2 : lang α) : lang α :=
--     λ w, any (range (length w + 1)) (λ i, take i w ∈ L1 ∧ drop i w ∈ L2)

-- lemma bor_assoc (a b c : bool) : a || b || c = a || (b || c) :=
--     by cases a; simp

-- lemma any_cons {α : Type} (p : α → bool) (x : α) (xs : list α) :
--     any (x :: xs) p = p x || any xs p :=
-- begin
--     unfold any,

solson

lemma range_core_step : ∀ (n : ℕ) (xs ys : list ℕ),
    range_core n (xs ++ ys) = range_core n xs ++ ys
| 0     xs ys := rfl
| (n+1) xs ys := by rw [range_core, range_core, ←cons_append, range_core_step]

lemma range_step (n : ℕ) : range (n.succ) = range n ++ [n] :=
    have h : range_core n [n] = range_core n (nil ++ [n]), by rw nil_append,
    by rw [range, range, range_core, h, range_core_step]

solson

lemma sizeof_drop_lt_sizeof {α : Type} {n : ℕ} {xs : list α} :
    list.sizeof (drop n xs) < 1 + list.sizeof xs :=
begin
    induction n generalizing xs,
    case nat.zero {
        apply nat.lt_add_of_pos_left,
        constructor,
    },
    case nat.succ n' ih_n {
        cases xs,

solson

foo