Identity Example - Elaborator Reflection

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> 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.