[Agda] Infinite proofs

Paolo Capriotti p.capriotti at gmail.com
Sat Apr 20 11:10:21 CEST 2013


On Sat, Apr 20, 2013 at 6:06 AM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> You can't prove them equal in Agda, and you probably shouldn't be able to in
> Coq either (it breaks subject reduction) but you can anyway.

Are you sure you can prove them *equal* in Coq? Chlipala only proves
that they are bisimilar.

Paolo


More information about the Agda mailing list