mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
9fab367f0f
On the LHS, we want to match against the reflected thing, so FC and implicits need to turn into match anything patterns, or we won't match anything at all. This means we can put quoted terms on the LHS, with pattern variables under ~().
25 lines
585 B
Idris
25 lines
585 B
Idris
import Language.Reflection
|
|
|
|
%language ElabReflection
|
|
|
|
solveReflected : TTImp -> Elab TT
|
|
solveReflected `(Builtin.Equal {a=_} {b=_} ~(left) ~(right))
|
|
= do logTerm 0 "Left" left
|
|
logTerm 0 "Right" right
|
|
fail "Not done"
|
|
solveReflected g
|
|
= do logTerm 0 "Goal" g
|
|
fail "I don't know how to prove this"
|
|
|
|
%macro
|
|
prove : Elab TT
|
|
prove
|
|
= do env <- localVars
|
|
Just g <- goal
|
|
| Nothing => fail "No goal to solve"
|
|
logMsg 0 (show env)
|
|
solveReflected g
|
|
|
|
commutes : (x, y : Nat) -> plus x y = plus y x
|
|
commutes x y = prove
|