mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
22 lines
617 B
JavaScript
22 lines
617 B
JavaScript
const $JSRTS = {
|
|
throw: function (x) {
|
|
throw x;
|
|
},
|
|
Lazy: function (e) {
|
|
this.js_idris_lazy_calc = e;
|
|
this.js_idris_lazy_val = void 0;
|
|
},
|
|
force: function (x) {
|
|
if (x === undefined || x.js_idris_lazy_calc === undefined) {
|
|
return x
|
|
} else {
|
|
if (x.js_idris_lazy_val === undefined) {
|
|
x.js_idris_lazy_val = x.js_idris_lazy_calc()
|
|
}
|
|
return x.js_idris_lazy_val
|
|
}
|
|
},
|
|
prim_strSubstr: function (offset, len, str) {
|
|
return str.substr(Math.max(0, offset), Math.max(0, len))
|
|
}
|
|
}; |