Class LIST

• Defined in theory: Kif-lists
• Source code: kif-lists.lisp

Slots on this class:

Documentation:

A list is a sequence --- an ordered bag --- of elements. It is KIF primitive.

Instance-Of: Class

Other Related Axioms:

(<=> (Null ?List) (And (List ?List) (= (Length ?List) 0)))

(=> (Listof $X $Y) (List $Y))

(<=> (Single ?List) (And (List ?List) (= (Length ?List) 1)))

(<=> (Double ?List) (And (List ?List) (= (Length ?List) 2)))

(<=> (Triple ?List) (And (List ?List) (= (Length ?List) 3)))

(=> (First $X $Y) (List $X))

(=> (Last $X $Y) (List $X))

(=> (Item $X $Y) (List $Y))

(=> (Sublist $X $Y) (List $Y))

(=> (Sublist $X $Y) (List $X))

(Nth-Domain Cons 3 List)

(Nth-Domain Cons 2 List)

(<- (Append ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Cons (First ?L1) (Append (Rest ?L1) ?L2))))

(Nth-Domain Append 3 List)

(Nth-Domain Append 2 List)

(Nth-Domain Append 1 List)

(<- (Revappend ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Revappend (Rest ?L1) (Cons (First ?L1) ?L2))))

(Nth-Domain Revappend 3 List)

(Nth-Domain Revappend 2 List)

(Nth-Domain Revappend 1 List)

(=> (Reverse $X $Y) (List $Y))

(=> (Reverse $X $Y) (List $X))

(Nth-Domain Adjoin 3 List)

(Nth-Domain Adjoin 2 List)

(<- (Remove ?X ?List)
    (Cond ((Null ?List) Nil)
          ((And (= ?X (First ?List)) (List ?List))
           (Remove ?X (Rest ?List)))
          ((List ?List) (Cons ?X (Remove ?X (Rest ?List))))))

(Nth-Domain Remove 3 List)

(Nth-Domain Remove 2 List)

(<- (Subst ?X ?Y ?Z)
    (Cond ((= ?Y ?Z) ?X)
          ((Null ?Z) Nil)
          ((List ?Z)
           (Cons (Subst ?X ?Y (First ?Z)) (Subst ?X ?Y (Rest ?Z))))
          (True ?Z)))

(<- (Length ?List)
    (Cond ((Null ?List) 0) ((List ?List) (1+ (Length (Rest ?List))))))

(=> (Length $X $Y) (List $X))

(Nth-Domain Nth 1 List)

(<- (Nthrest ?List ?N)
    (Cond ((= ?N 0) (If (List ?List) ?List))
          ((Positive ?N) (Nthrest (Rest ?List) (1- ?N)))))

(Nth-Domain Nthrest 3 List)

(Nth-Domain Nthrest 1 List)