PasteRack.org | ||
Paste # 57979 | ||
2019-02-17 10:01:52 | ||
Fork as a new paste. | ||
Paste viewed 71 times. | ||
Tweet | ||
Embed: | ||
#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]