Hi,
You asked for it :).
------------------------------------------------------------------------------
( p : Eq (cons a as) (cons b bs) !
let !--------------------------------!
! injCons p : Eq as bs )
injCons p <= case p
{ injCons (rfl (cons a as)) => rfl as
}
------------------------------------------------------------------------------
( p : Eq (cons a as) (cons b bs) !
let !--------------------------------!
! injCons2 p : Eq a b )
injCons2 p <= case p
{ injCons2 (rfl (cons a as)) => rfl a
}
------------------------------------------------------------------------------
( p1 : Dec (Eq a b) ; p2 : Dec (Eq as bs) !
let !----------------------------------------------------!
! decEqCons p1 p2 : Dec (Eq (cons a as) (cons b bs)) )
decEqCons p1 p2 <= case p1
{ decEqCons (yes a') p2 <= case p2
{ decEqCons (yes a'') (yes a) <= case a''
{ decEqCons (yes (rfl a)) (yes a') <= case a'
{ decEqCons (yes (rfl a)) (yes (rfl as)) => yes (rfl (cons a as))
}
}
decEqCons (yes a') (no f) => no (lam p => f (injCons p))
}
decEqCons (no f) p2 <= case p2
{ decEqCons (no f) (yes a) <= case a
{ decEqCons (no f) (yes (rfl as)) => no (lam p => f (injCons2 p))
}
decEqCons (no f') (no f) => no (lam p => f' (injCons2 p))
}
}
------------------------------------------------------------------------------
The first three cases are unsurprising, but when neither the heads nor
the tails are equal epigram accepts the explanation that the heads are
not equal. I expected that 'f' (ie that the tails are different too)
would have to appear on the rhs! Why does epigram allow me to lose that
information???
Thanks, Laszlo
Peter Morris wrote:
Hi all,
Sorry for the black out in coverage on the list recently (which you
may or may not have noticed) we should now be functional again, so if
you have been itching to ask a question or start a discussion then,
please, go ahead.
Peter
