Function FIRST

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

Slots on this function:

Instance-Of: Function

Arity: 2

Domain: List

Other Related Axioms:

(<- (First ?List)
    (If (Exists (@Items) (= (Listof ?X @Items) ?List)) ?X))

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

(<- (Last ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) (First ?List))
          (True (Last (Rest ?List)))))

(<- (Butlast ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) Nil)
          (True (Cons (First ?List) (Butlast (Rest ?List))))))

(=> (Item ?X ?List)
    (And (Not (Null ?List))
         (Or (= ?X (First ?List)) (Item ?X (Rest ?List)))))

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

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

(<- (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))))))

(<- (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)))

(<- (Nth ?List ?N)
    (Cond ((= ?N 1) (First ?List))
          ((Positive ?N) (Nth (Rest ?List) (1- ?N)))))