Proof tactics within source files?

[Dirk Ullrich]

Hello,

to learn more about dependently typed languages in practice I've
started to work through (parts of) the book "Software Foundations" of
Peirce et. al. (http://www.cis.upenn.edu/~bcpierce/sf/index.html).
This book is for learning Coq, but I try to do as many as possible of
the the examples and exercises in Agda and Idris, too.

Now I wonder whether there is any way to access Idris' proof tactics
from within an Idris source file (like it can be done, for instance,
in Coq).

Dirk

[Andrea Vezzosi]

There are some examples in the lib, e.g.:

https://github.com/edwinb/Idris-dev/blob/master/lib/prelude/nat.idr#L582

-- Andrea

[Dirk Ullrich]

Hello,

2012/7/26 Andrea Vezzosi <sanz...@gmail.com>:

> There are some examples in the lib, e.g.:
> https://github.com/edwinb/Idris-dev/blob/master/lib/prelude/nat.idr#L582

thank you for the tip, Andrea. Although I did RTFM (tutorial) I did
not look into the sources. So I've wrongly assumed that the
`:addproof' command in Idris' REPL will add proof *terms* to the
source file.

By the way: You can even get rid of the metavariables. Here is
primitive example for illustration:
If you have something like this in your source file:

or_tf : True || False = True
or_tf = ?or_tf_proof
...
?or_tf_proof = proof {
compute;
refine refl;
}

you could also write:

or_tf : True || False = True
or_tf = proof {
compute;
refine refl;
}

instead.

Dirk