Agda2 Examples: Extraction of Programs from Proofs for Real Number Computation

This page contains the source code in Agda which allows to carry out some real number computations in Agda using postulated types.

Evaluating example1/3 10 returns the first 10 digits of 1/3, similarly for example1/4 n, example-1/3 n, ...