[Agda] Platform Independent proofs.

[Apostolis Xekoukoulotakis]

I was trying to support floats in agda-ocaml when I realized that this is a
lost cause and a very dangerous one.

If I didn't match the exact computational results of haskell, then I could
get proofs that typechecked in agda that were completely wrong in OCaml.

But there is also a theoretical error in all of this. Right now, we do not
have universal proofs like in Mathematics. We have platform dependent
proofs.

In other words, we should write explicitly that this proof is correct for
this specific version of the CPU, this specific version of haskell etc.

Is it the job of agda to check whether two hardware or software versions
have the same computational results? Of course not.

In my opinion, all platform dependent computations should be inserted as
postulates. This way, agda will do exactly what it was programmed to do.

And we can still prove things for postulates.

```
open import Common.Integer
open import Agda.Builtin.Equality

postulate
  Float : Set
  d : Float
  round : Float → Integer

f : round d ≡ round d
f = refl
```
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190523/0af79dc3/attachment.html>