git.iko.soy/Idris-dev
on master help sign in
Fix typo in docstring for Tactics.apply
a297e02David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+1−1
compare with master
unifiedsplit
@@ -252,7 +252,7 @@ namespace Tactics
252 fill tm = prim__Fill tm
252 fill tm = prim__Fill tm
253
253
254 ||| Attempt to apply an operator to fill the current hole,
254 ||| Attempt to apply an operator to fill the current hole,
255− ||| potentially solving arugments by unification.
255+ ||| potentially solving arguments by unification.
256 |||
256 |||
257 ||| The return value is a list of pairs of names, one for each input
257 ||| The return value is a list of pairs of names, one for each input
258 ||| argument. The first projection of these pairs is the original
258 ||| argument. The first projection of these pairs is the original