mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
23 lines
916 B
Idris
23 lines
916 B
Idris
module Quasiquote005
|
|
|
|
-- Test Raw quasiquotes
|
|
|
|
test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =
|
|
RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))
|
|
(RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
|
|
(Var (NS (UN "Z") ["Nat", "Prelude"]))))
|
|
(RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
|
|
(Var (NS (UN "Z") ["Nat", "Prelude"])))
|
|
test = Refl
|
|
|
|
firstAddend : Raw -> Maybe Raw
|
|
firstAddend `(plus ~first ~_) = Just first
|
|
firstAddend _ = Nothing
|
|
|
|
firstAddendOk : firstAddend (RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))
|
|
(RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
|
|
(Var (NS (UN "Z") ["Nat", "Prelude"]))))
|
|
(Var (NS (UN "Z") ["Nat", "Prelude"]))) =
|
|
the (Maybe Raw) (Just `(S Z))
|
|
firstAddendOk = Refl
|