idris-0.9.20: jsrts/Runtime-browser.js

var i$getLine = function() {
    return prompt("Prelude.getLine");
}

var i$putStr = function(s) {
  console.log(s);
};

var i$systemInfo = function(index) {
  switch(index) {
    case 0:
      return "javascript";
    case 1:
      return navigator.platform;
  }
  return "";
}