Suppose I have a function in Idris that does some computation. For simplicity, let it be *stringly* typed for now.

```
f: String -> String

```

How can I compile this function to JavaScript so that it can then be called from any ordinary JavaScript code?

If that is too easy, suppose `f`, instead of `String`, deals with `Double` or even a custom Idris data type.

I know I can compile a whole module with a `Main.main` function and a more or less inscrutable blob of JavaScript will be output. Can I maybe extract my function from there by hand? How should I go about it?

---

**P.S.** Despite my answering myself, I am still looking for a better solution, so welcome.