I hadn't realised that Idris has a quasiquotes until I came across some tests in the test suite.
Here's a short example in the REPL:
Idris> :module Language.Reflection
Idris> `(S Z)
App (P (DCon 1 1)
(NS (UN "S") ["Nat", "Prelude"])
(Bind (MN 0 "_t")
(Pi (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)
(TType (UVar "./Prelude/Nat.idr" 22)))
(P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)))
(P (DCon 0 0)
(NS (UN "Z") ["Nat", "Prelude"])
(P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)) : TT
I'd like to understand what that's all about. A brief overview and/or some references would be appreciated!
Aucun commentaire:
Enregistrer un commentaire