[Agda] rewriting before defining

[Andreas Abel]

Well, the doctor could perform some surgery on Agda, take out the 
cancerous error message and see what happens. ;-)

I wash my hands in innocence.  For me, the intended use of REWRITE was 
to add a proven propositional equality to definitional equality; if you 
go beyond it, you have to worry about the semantics yourself.

Cheers,
Andreas

On 28.02.2018 19:07, Thorsten Altenkirch wrote:
> Hi,
> 
> I am mutually defining an equality and some other things. To be able to 
> type check the other things I need the equality as a rewriting rule but 
> agda doesn't let me.
> 
> That is I get the error
> Rewrite rule from function  Skm-∘  cannot be added before the function 
> definition
> when checking the pragma REWRITE Skm-∘
> when checking the attached file.
> 
> I know that I am cheating but I want to do it. Can I tell it that I am a 
> doctor and I know what I am doing. Otherwise I shouldn't be allowed to 
> use Rewrite anyway.
> 
> Yes, I can replace it by a postulate but that misses the point.
> 
> Cheers,
> Thorsten
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/