search

idris-hackers / software-foundations

Software Foundations in Idris
https://idris-hackers.github.io/software-foundations
MIT License
452 stars 34 forks source link

Imp #36

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

They spend a large chunk of this chapter introducing more tactics like try and omega. Some of those exist in Pruviloj, and the new tactics don't really get used in the remainder of the chapter, so we should probably move this part to the hypothetical Pruviloj chapter.

yurrriq commented 7 years ago

Sounds good to me.

clayrat commented 7 years ago

Should be ready for review.

I'm not too happy about introducing multiple names for AExp/CEval/etc but couldn't figure out how to compartmentalize them with namespaces.

yurrriq commented 7 years ago

Let's hold off on this until we finish up to Rel and push a new PDF.

yurrriq commented 7 years ago

If you want to merge this one too, go ahead, @clayrat.

clayrat commented 7 years ago

Let's do this one too