sdfsd.idr

-- Not compelete since it doesn't go to HasIO yet, but given:
-- makeHasIO "what" ["c:foo","javascript:borp"] `[ prim_gob : Int -> Int -> PrimIO Int ]
-- This generates:
-- %foreign "c:foo" "javascript:borp"
-- what : Int -> Int -> PrimIO Int
makeHasIO : String -> List String -> List Decl -> Elab ()
makeHasIO funname str ys = do
  [IClaim fc mw vis _ (MkTy tyfc _ ty)] <- pure ys
    | _ => fail "bad format"
  let r = IClaim fc mw vis [ForeignFn str] (MkTy tyfc (UN funname) ty)
  -- spits out what r is when :log 1 is set in repl
  quote r >>= logTerm "as" 1 "fds"
  declare [r]

%runElab makeHasIO "what" ["c:foo","javascript:borp"] `[ prim_gob : Int -> Int -> PrimIO Int ]