| First I created a file 'identity.idr' containing the following: | idNat : Nat -> Nat idNat = ?hole |
Then run Idris using this file:
| Start Idris | mjb@linux:~> cd Idris-dev2/libs/algebra
mjb@linux:~/Idris-dev2/libs/algebra> idris identity.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.hole |
*identity> :module Language.Reflection.Elab Holes: Main.hole |
|
| Start Elab | *identity> :elab hole
---------- Goal: ----------
{hole_0} : Nat -> Nat |
-Main.hole> :state
---------- Goal: ----------
{hole_0} : Nat -> Nat |
|
| Intro | -Main.hole> intro `{{x}}
---------- Assumptions: ----------
x : Nat
---------- Goal: ----------
{hole_0} : Nat |
| Fill | -Main.hole> fill (Var `{{x}})
---------- Assumptions: ----------
x : Nat
---------- Goal: ----------
{hole_0} : Nat =?= x |
| Solve | -Main.hole> solve hole: No more goals. |
| Exit Elab | -Main.hole> :qed
Proof completed!
Main.hole = %runElab (do intro `{{x}}
fill (Var `{{x}})
solve)
*identity> |
