solson

instance decidable_ex_lt (p : ℕ → Prop) [decidable_pred p] : ∀ (n : ℕ), decidable (∃ x < n, p x)
| 0     := is_false $ assume ⟨x, h_lt, _⟩, nat.not_lt_zero x h_lt
| (n+1) :=
    match decidable_ex_lt n with
    | is_true h :=
        is_true $ let ⟨x, h_lt, hp⟩ := h in ⟨x, nat.lt_succ_of_lt h_lt, hp⟩
    | is_false h_not :=
        if h_pn : p n
        then is_true ⟨n, nat.lt_succ_self n, h_pn⟩
        else is_false $ assume ⟨x, h_lt, h_px⟩,

solson

instance decidable_ex_fin {n : ℕ} (p : ℕ → Prop) [decidable_pred p] :
    decidable (∃ (x : fin n), p x) :=
match list.decidable_bex p (range n) with
| is_true h := is_true $
    let ⟨x, h_range, hp⟩ := h in ⟨⟨x, lt_of_mem_range h_range⟩, hp⟩
| is_false h_not := is_false $
    assume ⟨⟨x, is_lt⟩, hp⟩, h_not ⟨x, mem_range_of_lt is_lt, hp⟩
end

solson

lemma range_core_step (n : ℕ) (xs ys : list ℕ) :
    range_core n (xs ++ ys) = range_core n xs ++ ys :=
begin
    induction n generalizing xs ys,
    case nat.zero { refl },
    case nat.succ n' ih_n {
        unfold range_core,
        rewrite ←cons_append,
        rewrite ih_n,
    },

solson

def range_fin : ∀ n : ℕ, list (fin n)
| 0     := []
| (n+1) := 0 :: map fin.succ (range_fin n)

def range_fin_core' {n : ℕ} : fin (n + 1) → list (fin n) → list (fin n)
| ⟨0, _⟩   xs := xs
| ⟨x+1, h⟩ xs :=
    have x < n, from nat.lt_of_succ_lt_succ h,
    have x < n + 1, from nat.lt_of_succ_lt h,
    range_fin_core' ⟨x, ‹x < n + 1›⟩ (⟨x, ‹x < n›⟩ :: xs)

solson

lemma app_take_drop {α: Type} (n : ℕ) (xs : list α) : xs = take n xs ++ drop n xs :=
begin
    induction n generalizing xs,
    case nat.zero { refl },
    case nat.succ n' ih_n {
        cases xs,
        case nil { refl },
        case cons x' xs' { rewrite [take, drop, cons_append, ←ih_n xs'] },
    },
end

solson

lemma drop_sizeof_lt {α : Type} {n : ℕ} {xs : list α} :
    list.sizeof (drop n xs) < 1 + list.sizeof xs :=
begin
    induction n with n' ih_n generalizing xs,
    { apply nat.lt_add_of_pos_left, constructor },
    {
        cases xs with x' xs',
        { unfold list.sizeof, constructor },
        {
            unfold drop,

solson

theorem not_not_lem {p : Prop} : ¬¬(p ∨ ¬p) :=
    assume not_lem : ¬(p ∨ ¬p),
    have not_p : ¬p, from not_lem ∘ or.inl,
    have not_not_p : ¬¬p, from not_lem ∘ or.inr,
    absurd not_p not_not_p

theorem lem_implies_dne (lem : ∀ {q : Prop}, q ∨ ¬q) {p : Prop} : ¬¬p → p :=
    assume not_not_p : ¬¬p,
    match lem with
    | or.inl p := p

solson

%default total

postulate callCC : ((a -> Void) -> a) -> a

excludedMIddle : Dec a
excludedMiddle = callCC (\assumption => No (\contradiction => void (assumption (Yes y))))

solson

pub ExprFunction: Expr = {
    <i:ID> ":" <e:ExprFunction> => unimplemented!("lambda({:?}, {:?})", i, e),
    "{" <f:Formals> "}" ":" <e:ExprFunction> => unimplemented!("lambda({:?}, {:?})", f, e),
    <i:ID> => Expr::Identifier(Symbol::new(i)), // TODO: wrong place
};

solson

static Expr * stripIndentation(const Pos & pos, SymbolTable & symbols, vector<Expr *> & es)
{
    if (es.empty()) return new ExprString(symbols.create(""));

    /* Figure out the minimum indentation.  Note that by design
       whitespace-only final lines are not taken into account.  (So
       the " " in "\n ''" is ignored, but the " " in "\n foo''" is.) */
    bool atStartOfLine = true; /* = seen only whitespace in the current line */
    unsigned int minIndent = 1000000;
    unsigned int curIndent = 0;