Chuangjie Xu, January 2017

We implement the term extraction algorithm via a nonstandard
Dialectica interpretation for system H introduced in

   B. van den Berg, E. Briseid, and P. Safarik, A functional
   interpretation for nonstandard arithmetic, Annals of pure
   and applied logic 163 (2012), no. 12, 1962–1994.

We define system H with 4 inductive datatypes

\begin{code}

import H

\end{code}

and then the term extraction algorithm via a nonstandard Dialectica
interpretation.

\begin{code}

import Dialectica

\end{code}

Extracted terms contain noncomputational information. So we define a
simplify function to remove it.

\begin{code}

import Simp

\end{code}

In the end We present a few simple examples and compare the terms
extracted from different proofs of a theorem.

\begin{code}

import Examples

\end{code}