cleanup

Author: andrevidela

src/Core/WithData.idr

@@ -199,14 +199,12 @@ public export
 TyName' : KeyVal
 TyName' = "name" :-: FCBind Name
 
-namespace TypeName
-  ||| Extract the "tyname" value from the metadata record
-  export
-  (.tyName) : {n : Nat} ->
-            (inRange : NameInRange "name" fields === Just (n, FCBind Name)) =>
-            WithData fields a -> FCBind Name
-  (.tyName) = WithData.get "name" @{inRange}
-
+||| Extract the "tyname" value from the metadata record
+export
+(.tyName) : {n : Nat} ->
+          (inRange : NameInRange "name" fields === Just (n, FCBind Name)) =>
+          WithData fields a -> FCBind Name
+(.tyName) = WithData.get "name" @{inRange}
 
 ||| Attach documentation, binding and location information to a type
 public export

src/Idris/Elab/Interface.idr

@@ -190,7 +190,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths bindNames params
          let tydecl = IClaim (MkFCVal vfc $ MkIClaimData sig.count vis (if sig.isData then [Inline, Invertible]
                                             else [Inline])
                                       (Mk [vfc, NotBinding :+ cn] ty_imp))
-         let conapp = apply (IVar vfc cname) (map (IBindVar EmptyFC) allmeths)
+         let conapp = apply (IVar vfc cname) (map (IBindVar EmptyFC) bindNames)
          let argns = getExplicitArgs 0 sig.type
          -- eta expand the RHS so that we put implicits in the right place
          let fnclause = PatClause vfc