Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/Output

Created June 25, 2014 14:12
Show Gist options
  • Save david-christiansen/22e6df9bcab1e42d4ae5 to your computer and use it in GitHub Desktop.
Save david-christiansen/22e6df9bcab1e42d4ae5 to your computer and use it in GitHub Desktop.
Download ZIP
Beginning of quasiquotes for proof automation
Raw
Output
drc@drc:~/tmp$ idris Quasiquote.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.13.1-git:f8ec244
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./Quasiquote.idr
*Quasiquote> thing
App (App (App (P (DCon 1 3)
(NS (UN "::") ["List", "Prelude"])
(Bind (UN "a")
(Pi (TType (UVar -1)))
(Bind (MN 0 "_t")
(Pi (V 0))
(Bind (MN 2 "_t")
(Pi (App (P (TCon 0 0)
(NS (UN "List")
["List", "Prelude"])
Erased)
(V 1)))
(App (P (TCon 0 0)
(NS (UN "List") ["List", "Prelude"])
Erased)
(V 2))))))
(TType (UVal 0)))
(TType (UVal 0)))
(App (App (App (P (DCon 1 3)
(NS (UN "::") ["List", "Prelude"])
(Bind (UN "a")
(Pi (TType (UVar -1)))
(Bind (MN 0 "_t")
(Pi (V 0))
(Bind (MN 2 "_t")
(Pi (App (P (TCon 0 0)
(NS (UN "List")
["List", "Prelude"])
Erased)
(V 1)))
(App (P (TCon 0 0)
(NS (UN "List")
["List", "Prelude"])
Erased)
(V 2))))))
(TType (UVal 0)))
(P (TCon 15 0)
(NS (UN "Nat") ["Nat", "Prelude"])
(TType (UVar -1))))
(App (P (DCon 0 1)
(NS (UN "Nil") ["List", "Prelude"])
(Bind (UN "a")
(Pi (TType (UVar -1)))
(App (P (TCon 0 0)
(NS (UN "List") ["List", "Prelude"])
Erased)
(V 0))))
(TType (UVal 0)))) : TT
*Quasiquote>
Raw
Quasiquote.idr
module Quasiquote
import Language.Reflection
import Language.Reflection.Utils
nat : TT
nat = `(Nat)
three : TT
three = `(S (S (S Z)))
twoElems : TT
twoElems = `(with List [(), ()])
thing : TT
thing = `(with List [Type, ~nat])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment