Zulip Chat Archive

Stream: general

Topic: getting confused by 'abstract'


view this post on Zulip Scott Morrison (Jun 16 2018 at 10:28):

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'

view this post on Zulip Scott Morrison (Jun 16 2018 at 10:51):

Ah... writing lemma instead of def.


Last updated: May 11 2021 at 00:31 UTC