#lang pie

;; <=
(claim zero<=?
  (-> Nat Nat))
(define zero<=?
  (lambda (j)
    1))

(claim step-<=?
  (-> Nat (-> Nat Nat)
      (-> Nat Nat)))
(define step-<=?
  (lambda (n-1 n-1<=?)
    (lambda (j)
      (rec-Nat j
        0
        (lambda (j-1 almost_j-1)
          (n-1<=? j-1))))))


(claim <=? (-> Nat Nat Nat))
(define <=?
  (lambda (n j)
    ((rec-Nat n
       zero<=?
       step-<=?) j)))

;; insert :: Ord a => a -> [a] -> [a]
;; insert x [] = [x]
;; insert x (y:ys) 
;;         |  x < y = x:y:ys
;;         | otherwise = y : insert x ys

(claim step-insert
  (-> Nat Nat (List Nat) (List Nat)
      (List Nat)))
(define step-insert
  (lambda (x)
    (lambda (y ys result_ys)
      (which-Nat (<=? x y)
        (:: y result_ys)
        (lambda (_)
          (:: x (:: y ys) ) )))))

(claim insert
  (-> Nat (List Nat)
      (List Nat)))
(define insert
  (lambda (x list)
    (rec-List list
      (:: x nil)
      (step-insert x))))

standard-module-name-resolver: collection not found
  for module path: (submod pie reader)
  collection: "pie"
  in collection directories:
   /home/pasterack/.racket/6.8/collects
   /home/pasterack/racket68/collects
   ... [161 additional linked and package directories]
  context...:
   show-collection-err
   standard-module-name-resolver
   /home/pasterack/racket68/share/pkgs/scribble-lib/scribble/private/manual-code.rkt:112:0: get-tokens
   /home/pasterack/racket68/share/pkgs/scribble-lib/scribble/private/manual-code.rkt:56:0: typeset-code15
   /home/pasterack/pasterack/tmp/13574/13574code.scrbl: [running body]
   loop
   ...cket/cmdline.rkt:179:51
   /home/pasterack/racket68/share/pkgs/scribble-lib/scribble/run.rkt: [running body]