ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

Fix docstring

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-09-10 14:14:57 +02:00
parent 752a2fcc77
commit b28fecf6d2
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libs/prelude/Language/Reflection/Elab.idr
View File

@ -374,7 +374,8 @@ namespace Tactics
whnf : (term : TT) -> Elab TT
whnf term = prim__Whnf term
||| Check that two terms are convertable in the current context and environment
||| Check that two terms are convertable in the current context and
||| in some environment.
|||
||| @ env a lexical environment to compare the terms in (see `getEnv`)
||| @ term1 the first term to convert