coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "John Wiegley" <johnw AT newartisans.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Replace does not work
- Date: Tue, 07 Oct 2014 15:48:11 -0500
- Organization: New Artisans LLC
>>>>> Adam Chlipala
>>>>> <adamc AT csail.mit.edu>
>>>>> writes:
> Most likely the term you're giving to replace doesn't match the one found in
> the subgoal, considering implicit arguments, notations, etc. Try running
> [Set Printing All], and using a tactic like [pose] to bring the arguments to
> [replace] into the subgoal, so you can compare them against what appeared
> originally.
Yes, I run into this exact issue quite regularly, where sometimes a value was
destructed too late, so that some values in scope have the original form, and
others have the destructed form, but you can only see this difference using
Set Printing All. For example: where "fmap" is one case uses a Functor
instance in scope, while another "fmap" is using an "is_functor" coercion from
the Monad in scope.
John
- [Coq-Club] Replace does not work, Marcus Ramos, 10/07/2014
- Re: [Coq-Club] Replace does not work, Adam Chlipala, 10/07/2014
- Re: [Coq-Club] Replace does not work, John Wiegley, 10/07/2014
- Re: [Coq-Club] Replace does not work, Marcus Ramos, 10/08/2014
- Re: [Coq-Club] Replace does not work, Adam Chlipala, 10/07/2014
Archive powered by MHonArc 2.6.18.