PasteRack.org
Paste # 57979
2019-02-17 10:01:52

Fork as a new paste.

Paste viewed 71 times.


Embed:

implement of <=? is easy when encoding Boolean as Nat (0 and 1)

#lang pie

;; mylte : Nat -> Nat -> Nat
;; mylte Z j = 1
;; mylte (S k) Z = 0
;; mylte (S k) (S j) = mylte k j
(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)))

=>

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/57979/57979code.scrbl: [running body]
   loop
   ...cket/cmdline.rkt:179:51
   /home/pasterack/racket68/share/pkgs/scribble-lib/scribble/run.rkt: [running body]