Ramsay Taylor

Pre-submit checklist: - Branch - [x] Commit sequence broadly makes sense - [x] Key commits have useful messages - [x] Changelog fragments have been written (if appropriate) - [x] Relevant...

The files involved, the number of lines, and the estimated percentage of documentation completion (0 is no documentation at all, 100 is documentation is completed). File | Number of lines...

### Describe the feature you'd like The files involved, the number of lines, and the estimated percentage of documentation completion (0 is no documentation at all, 100 is documentation is...

Phil Wadler suggests some proofs to show the correspondence of the decidable definition of FD to the more clearly semantically valid pureFD.

The UFloatDelay translation relation requires a test that a term `isPure`. This exists in Haskell but needs defining in Agda. Currently it is a null type that accepts any term,...