Skip to content

Instantly share code, notes, and snippets.

Created May 1, 2017 10:35
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anonymous/2c8a0ce1f68845bb9884cbc444e12a35 to your computer and use it in GitHub Desktop.
Save anonymous/2c8a0ce1f68845bb9884cbc444e12a35 to your computer and use it in GitHub Desktop.
module Try1 where
open import Agda.Builtin.List
open import Agda.Builtin.String
e0 : List String
e0 = []
e1 : List String
e1 = "a" ∷ []
--------------
js result:
_jAgdaTry.e0 -> function (x0) { return x0["[]"](); }
_jAgdaTry.e1 ->
function (x2) {
return x2["_∷_"](x0, x1);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment