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> |