Agda 7b48a62 compiles this code
open import Agda.Builtin.Nat open import Agda.Builtin.Bool rng : Bool → Nat → Nat rng _ _ = 4 flip : (Bool → Nat → Nat) → (Nat → Bool → Nat) flip f a b = f b a rng' : Nat → Bool → Nat rng' = flip rng
to this JavaScript
var agdaRTS = require("agda-rts");
var z_jAgda_Agda_Builtin_Bool = require("jAgda.Agda.Builtin.Bool");
var z_jAgda_Agda_Builtin_Nat = require("jAgda.Agda.Builtin.Nat");
var z_jAgda_Agda_Primitive = require("jAgda.Agda.Primitive");
exports["flip"] = a => b => c => a(c)(b);
exports["rng"] = agdaRTS.primIntegerFromString("4");
exports["rng'"] = exports["flip"](exports["rng"]);
which is broken because exports["flip"] expects a function,
but is passed exports["rng"], which Agda has optimized to a literal.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4