(index ("list->tuple" 0) ("tuple" 227) ("tuple->list" 387) ("tuple->vector" 568) ("tuple-append" 757) ("tuple-butleft" 1060) ("tuple-butright" 1393) ("tuple-cons-left" 1714) ("tuple-cons-right" 2008) ("tuple-copy" 2305) ("tuple-empty?" 2483) ("tuple-eq?" 2659) ("tuple-eql?" 2871) ("tuple-equal?" 3129) ("tuple-eqv?" 3350) ("tuple-find" 3565) ("tuple-for-each" 3909) ("tuple-from-upto" 4319) ("tuple-head" 5019) ("tuple-left" 5285) ("tuple-length" 5510) ("tuple-map" 5698) ("tuple-of?" 6153) ("tuple-ref" 6336) ("tuple-reverse" 6598) ("tuple-right" 6872) ("tuple-split" 7101) ("tuple-tail" 7434) ("tuple?" 7742) ("vector->tuple" 7900) ("triple" 8175) ("triple->tuple" 8337) ("triple-eq?" 8577) ("triple-eql?" 8794) ("triple-equal?" 9072) ("triple-eqv?" 9298) ("triple-left" 9518) ("triple-middle" 9703) ("triple-right" 9899) ("triple?" 10088) ("couple" 10245) ("couple->tuple" 10403) ("couple-eq?" 10643) ("couple-eql?" 10860) ("couple-equal?" 11123) ("couple-eqv?" 11349) ("couple-left" 11569) ("couple-right" 11754) ("couple?" 11943) ("single" 12100) ("single-eq?" 12254) ("single-eql?" 12471) ("single-equal?" 12734) ("single-eqv?" 12960) ("single-ref" 13180) ("single-set!" 13362) ("single?" 13580))
(def (sig (procedure "(list->tuple lst)" (id list->tuple))) (p "function (result)") (highlight scheme "\n(list->tuple lst)\n\nrequires (list? lst)\n\nensures  (and (%tuple? result) (= (length lst) (%tuple-length result)))\n"))
(def (sig (procedure "(tuple . args)" (id tuple))) (p "function (result)") (highlight scheme "\n(tuple . args)\n\nrequires #t\n\nensures  (%tuple? result)\n"))
(def (sig (procedure "(tuple->list tup)" (id tuple->list))) (p "function (result)") (highlight scheme "\n(tuple->list tup)\n\nrequires (%tuple? tup)\n\nensures  (list? result)\n"))
(def (sig (procedure "(tuple->vector tup)" (id tuple->vector))) (p "function (result)") (highlight scheme "\n(tuple->vector tup)\n\nrequires (%tuple? tup)\n\nensures  (vector? result)\n"))
(def (sig (procedure "(tuple-append . tups)" (id tuple-append))) (p "function (result)") (highlight scheme "\n(tuple-append . tups)\n\nrequires ((list-of? %tuple?) tups)\n\nensures  (and (%tuple? result)\n              (= (tuple-length result)\n                 (apply + (map tuple-length tups))))\n"))
(def (sig (procedure "(tuple-butleft tup)" (id tuple-butleft))) (p "function (result)") (highlight scheme "\n(tuple-butleft tup)\n\nrequires (and (%tuple? tup)\n              (positive? (%tuple-length tup)))\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (- (%tuple-length tup) 1)))\n"))
(def (sig (procedure "(tuple-butright tup)" (id tuple-butright))) (p "function (result)") (highlight scheme "\n(tuple-butright tup)\n\nrequires (and (%tuple? tup) (positive? (%tuple-length tup)))\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (- (%tuple-length tup) 1)))\n"))
(def (sig (procedure "(tuple-cons-left arg tup)" (id tuple-cons-left))) (p "function (result)") (highlight scheme "\n(tuple-cons-left arg tup)\n\nrequires (%tuple? tup)\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (+ (%tuple-length tup) 1)))\n"))
(def (sig (procedure "(tuple-cons-right arg tup)" (id tuple-cons-right))) (p "function (result)") (highlight scheme "\n(tuple-cons-right arg tup)\n\nrequires (%tuple? tup)\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (+ (%tuple-length tup) 1)))\n"))
(def (sig (procedure "(tuple-copy tup)" (id tuple-copy))) (p "function (result)") (highlight scheme "\n(tuple-copy tup)\n\nrequires (%tuple tup)\n\nensures  (%tuple result)\n"))
(def (sig (procedure "(tuple-empty? xpr)" (id tuple-empty?))) (p "function (result)") (highlight scheme "\n(tuple-empty? xpr)\n\nrequires #t\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(tuple-eq? tup0 tup1)" (id tuple-eq?))) (p "function (result)") (highlight scheme "\n(tuple-eq? tup0 tup1)\n\nrequires (and (%tuple? tup0) (%tuple? tup1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(tuple-eql? eql? tup0 tup1)" (id tuple-eql?))) (p "function (result)") (highlight scheme "\n(tuple-eql? eql? tup0 tup1)\n\nrequires (and (procedure? eql?)\n              (%tuple? tup0) (%tuple? tup1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(tuple-equal? tup0 tup1)" (id tuple-equal?))) (p "function (result)") (highlight scheme "\n(tuple-equal? tup0 tup1)\n\nrequires (and (%tuple? tup0) (%tuple? tup1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(tuple-eqv? tup0 tup1)" (id tuple-eqv?))) (p "function (result)") (highlight scheme "\n(tuple-eqv? tup0 tup1)\n\nrequires (and (%tuple? tup0) (%tuple? tup1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(tuple-find ok? tup)" (id tuple-find))) (p "function (result)") (highlight scheme "\n(tuple-find ok? tup)\n\nrequires (and (procedure? ok?) (%tuple? tup))\n\nensures  (or (not result)\n             (and (cardinal? result)\n                  (< result (%tuple-length tup))\n                  \"index of found item\"))\n"))
(def (sig (procedure "(tuple-for-each proc tup . tups)" (id tuple-for-each))) (p "command ((old new (lambda (proc tup . tups) #t)))") (highlight scheme "\n(tuple-for-each proc tup . tups)\n\nrequires (and (procedure? proc)\n              (%tuple tup)\n              ((list-of? %tuple?) tups)\n              (apply = (%tuple-length tup) (map %tuple-length tups)))\n\nensures  \"proc applied to each item\"\n"))
(def (sig (procedure "(tuple-from-upto tup . interval)" (id tuple-from-upto))) (p "function (result)") (highlight scheme "\n(tuple-from-upto tup . interval)\n\nrequires (and (%tuple tup)\n              ((list-of? (lambda (x)\n                           (and (cardinal? x)\n                           (<= x (%tuple-length tup))))) interval)\n              (<= (length interval) 2) (apply <= 0 interval))\n\nensures  (and (%tuple? result)\n              (= (%tuple-length result)\n                 (case (length interval)\n\t\t\t\t\t\t\t\t\t ((0) (%tuple-length tup))\n\t\t\t\t\t\t\t\t\t ((1) (- (%tuple-length tup) (car interval)))\n\t\t\t\t\t\t\t\t\t ((2) (- (cadr interval) (car interval))))))\n"))
(def (sig (procedure "(tuple-head tup n)" (id tuple-head))) (p "function (result)") (highlight scheme "\n(tuple-head tup n)\n\nrequires (and (%tuple? tup)\n              (<= n (%tuple-length tup)))\n\nensures  (and (%tuple result) (= (%tuple-length result) n))\n"))
(def (sig (procedure "(tuple-left tup)" (id tuple-left))) (p "function (result)") (highlight scheme "\n(tuple-left tup)\n\nrequires (and (%tuple? tup) (positive? (%tuple-length tup)))\n\nensures  \"tup's leftmost item\"\n"))
(def (sig (procedure "(tuple-length tup)" (id tuple-length))) (p "function (result)") (highlight scheme "\n(tuple-length tup)\n\nrequires (%tuple? tup)\n\nensures  (cardinal? result)\n"))
(def (sig (procedure "(tuple-map fn tup . tups)" (id tuple-map))) (p "function (result)") (highlight scheme "\n(tuple-map fn tup . tups)\n\nrequires (and (procedure? fn)\n              (%tuple? tup)\n              ((list-of? %tuple?) tups)\n              (apply = (%tuple-length tup)\n                       (map %tuple-length tups)))\n\nensures  (and (%tuple? result)\n              (= (%tuple-length tup)\n                 (%tuple-length result)))\n"))
(def (sig (procedure "(tuple-of? ok?)" (id tuple-of?))) (p "function (result)") (highlight scheme "\n(tuple-of? ok?)\n\nrequires (procedure? ok?)\n\nensures  (procedure? result)\n"))
(def (sig (procedure "(tuple-ref tup n)" (id tuple-ref))) (p "function (result)") (highlight scheme "\n(tuple-ref tup n)\n\nrequires (and (%tuple? tup)\n              (cardinal? n)\n              (< -1 n (%tuple-length tup)))\n\nensures  \"tup's nth item\"\n"))
(def (sig (procedure "(tuple-reverse tup)" (id tuple-reverse))) (p "function (result)") (highlight scheme "\n(tuple-reverse tup)\n\nrequires (%tuple? tup)\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (%tuple-length tup)))\n"))
(def (sig (procedure "(tuple-right tup)" (id tuple-right))) (p "function (result)") (highlight scheme "\n(tuple-right tup)\n\nrequires (and (%tuple? tup) (positive? (%tuple-length tup)))\n\nensures  \"tup's rightmost item\"\n"))
(def (sig (procedure "(tuple-split tup at)" (id tuple-split))) (p "function (head tail)") (highlight scheme "\n(tuple-split tup at)\n\nrequires (and (%tuple? tup)\n          (cardinal? at) (< at (%tuple-length tup)))\n\nensures (and (%tuple? head) (%tuple? tail)\n          (%tuple-eql? equal? tup (%tuple-append head tail)))))\n"))
(def (sig (procedure "(tuple-tail tup n)" (id tuple-tail))) (p "function (result)") (highlight scheme "\n(tuple-tail tup n)\n\nrequires (and (%tuple? tup) (<= n (%tuple-length tup)))\n\nensures  (and (%tuple result)\n              (= (%tuple-length result)\n                 (- (%tuple-length tup) n)))\n"))
(def (sig (procedure "(tuple? xpr)" (id tuple?))) (p "function (result)") (highlight scheme "\n(tuple? xpr)\n\nrequires #t\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(vector->tuple vec)" (id vector->tuple))) (p "function (result)") (highlight scheme "\n(vector->tuple vec)\n\nrequires (vector? vec)\n\nensures  (and (%tuple? result)\n              (= (%tuple-length result)\n                 (vector-length vec)))\n"))
(def (sig (procedure "(triple x y z)" (id triple))) (p "function (result)") (highlight scheme "\n(triple x y z)\n\nrequires #t\n\nensures  (%triple? result)\n"))
(def (sig (procedure "(triple->tuple trp)" (id triple->tuple))) (p "function (result)") (highlight scheme "\n(triple->tuple trp)\n\nrequires (%triple? trp)\n\nensures  (and (%tuple? result)\n              (= (%tuple-length result) 3))\n"))
(def (sig (procedure "(triple-eq? trp0 trp1)" (id triple-eq?))) (p "function (result)") (highlight scheme "\n(triple-eq? trp0 trp1)\n\nrequires (and (%triple? trp0) (%triple? trp1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(triple-eql? eql? trp0 trp1)" (id triple-eql?))) (p "function (result)") (highlight scheme "\n(triple-eql? eql? trp0 trp1)\n\nrequires (and (procedure? eql?)\n              (%triple? trp0)\n              (%triple? trp1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(triple-equal? trp0 trp1)" (id triple-equal?))) (p "function (result)") (highlight scheme "\n(triple-equal? trp0 trp1)\n\nrequires (and (%triple? trp0) (%triple? trp1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(triple-eqv? trp0 trp1)" (id triple-eqv?))) (p "function (result)") (highlight scheme "\n(triple-eqv? trp0 trp1)\n\nrequires (and (%triple? trp0) (%triple? trp1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(triple-left trp)" (id triple-left))) (p "function (result)") (highlight scheme "\n(triple-left trp)\n\nrequires (%triple? trp)\n\nensures  \"leftmost item\"\n"))
(def (sig (procedure "(triple-middle trp)" (id triple-middle))) (p "function (result)") (highlight scheme "\n(triple-middle trp)\n\nrequires (%triple? trp)\n\nensures  \"item in the middle\"\n"))
(def (sig (procedure "(triple-right trp)" (id triple-right))) (p "function (result)") (highlight scheme "\n(triple-right trp)\n\nrequires (%triple? trp)\n\nensures  \"rightmost item\"\n"))
(def (sig (procedure "(triple? x)" (id triple?))) (p "function (result)") (highlight scheme "\n(triple? x)\n\nrequires #t\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(couple x y)" (id couple))) (p "function (result)") (highlight scheme "\n(couple x y)\n\nrequires #t\n\nensures  (%couple? result)\n"))
(def (sig (procedure "(couple->tuple cpl)" (id couple->tuple))) (p "function (result)") (highlight scheme "\n(couple->tuple cpl)\n\nrequires (%couple? cpl)\n\nensures  (and (%tuple? result)\n              (= (%tuple-length result) 2))\n"))
(def (sig (procedure "(couple-eq? cpl0 cpl1)" (id couple-eq?))) (p "function (result)") (highlight scheme "\n(couple-eq? cpl0 cpl1)\n\nrequires (and (%couple? cpl0) (%couple? cpl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(couple-eql? eql? cpl0 cpl1)" (id couple-eql?))) (p "function (result)") (highlight scheme "\n(couple-eql? eql? cpl0 cpl1)\n\nrequires (and (procedure? eql?)\n              (%couple? cpl0) (%couple? cpl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(couple-equal? cpl0 cpl1)" (id couple-equal?))) (p "function (result)") (highlight scheme "\n(couple-equal? cpl0 cpl1)\n\nrequires (and (%couple? cpl0) (%couple? cpl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(couple-eqv? cpl0 cpl1)" (id couple-eqv?))) (p "function (result)") (highlight scheme "\n(couple-eqv? cpl0 cpl1)\n\nrequires (and (%couple? cpl0) (%couple? cpl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(couple-left cpl)" (id couple-left))) (p "function (result)") (highlight scheme "\n(couple-left cpl)\n\nrequires (%couple? cpl)\n\nensures  \"leftmost item\"\n"))
(def (sig (procedure "(couple-right cpl)" (id couple-right))) (p "function (result)") (highlight scheme "\n(couple-right cpl)\n\nrequires (%couple? cpl)\n\nensures  \"rightmost item\"\n"))
(def (sig (procedure "(couple? x)" (id couple?))) (p "function (result)") (highlight scheme "\n(couple? x)\n\nrequires #t\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(single x)" (id single))) (p "function (result)") (highlight scheme "\n(single x)\n\nrequires #t\n\nensures  (%single? result)\n"))
(def (sig (procedure "(single-eq? sgl0 sgl1)" (id single-eq?))) (p "function (result)") (highlight scheme "\n(single-eq? sgl0 sgl1)\n\nrequires (and (%single? sgl0) (%single? sgl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(single-eql? eql? sgl0 sgl1)" (id single-eql?))) (p "function (result)") (highlight scheme "\n(single-eql? eql? sgl0 sgl1)\n\nrequires (and (procedure? eql?)\n              (%single? sgl0) (%single? sgl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(single-equal? sgl0 sgl1)" (id single-equal?))) (p "function (result)") (highlight scheme "\n(single-equal? sgl0 sgl1)\n\nrequires (and (%single? sgl0) (%single? sgl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(single-eqv? sgl0 sgl1)" (id single-eqv?))) (p "function (result)") (highlight scheme "\n(single-eqv? sgl0 sgl1)\n\nrequires (and (%single? sgl0) (%single? sgl1))\n\nensures  (boolean? result)\n"))
(def (sig (procedure "(single-ref sg)" (id single-ref))) (p "function (result)") (highlight scheme "\n(single-ref sg)\n\nrequires (%single? sg)\n\nensures  \"sg's stored item\"\n"))
(def (sig (procedure "(single-set! sg x)" (id single-set!))) (p "command ((old new (lambda (sg x) (%single-ref sg))))") (highlight scheme "\n(single-set! sg x)\n\nrequires (%single? sg)\n\nensures  (equal? new x)\n"))
(def (sig (procedure "(single? x)" (id single?))) (p "function (result)") (highlight scheme "\n(single? x)\n\nrequires #t\n\nensures  (boolean? result)\n"))
