idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-07 08:18:12 +03:00
Code Issues Projects Releases Wiki Activity

undo unneeded export

Browse Source
This commit is contained in:
Mathew Polzin 2021-01-03 11:53:20 -08:00
parent 0b0c9b33a4
commit b9bd65a497
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/TTImp/Interactive/ExprSearch.idr
View File

@ -710,7 +710,6 @@ tryIntermediateRec fc rig opts env ty topty (Just rd)
pure True
isSingleCon _ _ = pure False
export
searchType : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->