aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/list.spad.pamphlet
diff options
context:
space:
mode:
Diffstat (limited to 'src/algebra/list.spad.pamphlet')
-rw-r--r--src/algebra/list.spad.pamphlet10
1 files changed, 7 insertions, 3 deletions
diff --git a/src/algebra/list.spad.pamphlet b/src/algebra/list.spad.pamphlet
index 7290f770..2ac22b9f 100644
--- a/src/algebra/list.spad.pamphlet
+++ b/src/algebra/list.spad.pamphlet
@@ -268,9 +268,13 @@ List(S:Type): Exports == Implementation where
Implementation ==>
IndexedList(S, LISTMININDEX) add
- nil == NIL$Lisp
- null l == NULL(l)$Lisp
- cons(s, l) == CONS(s, l)$Lisp
+ import %nil: % from Foreign Builtin
+ import %peq: (%,%) -> Boolean from Foreign Builtin
+ import %makepair: (S,%) -> S from Foreign Builtin
+
+ nil == %nil
+ null l == %peq(l,%nil)
+ cons(s, l) == %makepair(s,l)
append(l:%, t:%) == APPEND(l, t)$Lisp
if S has OpenMath then