a bug in backchain?

15 views
Skip to first unread message

Gopalan Nadathur

unread,
May 14, 2018, 11:26:04 AM5/14/18
to Abella
Looks like backchain is forgetting the annotation on atomic goals when matching. This does not seem to be correct as the following development and "proof" shows:

Type q  prop.

Define p : prop by
  p := true.

Theorem cont : p -> q.
  induction on 1. intros. assert p. backchain IH. backchain H2.

Kaustuv Chaudhuri

unread,
May 14, 2018, 12:05:13 PM5/14/18
to Abella
Thanks for the report. This is now fixed.


Kaustuv
Reply all
Reply to author
Forward
0 new messages