getting confused by 'abstract'

Stream: general

[Scott Morrison]

I'm really confused by abstract. I've used it successfully in the past, but tonight it just won't do anything for me. Can anyone see what's wrong with this:

open tactic

structure C :=
(a : ℕ)
(b : a > 0)
(c : array a ℕ)

lemma H : C :=
begin
abstract foo { split, rotate 2, exact 1, abstract { exact dec_trivial }, split, abstract bar { intros, exact 0 } }
end

set_option pp.proofs true
#print H   -- theorem H : C := {a := 1, b := of_as_true trivial, c := {data := λ (i : fin 1), 0}}
#print foo -- 'unknown identifier foo'
#print bar -- 'unknown identifier bar'

[Scott Morrison]

Ah... writing lemma instead of def.