vertices-dump.rkt

(ℬ (tree) … ((tree ↦ tree_₂)))
↦

;;;;; ok cases

;; `tree` is either a number, in which case `vertices` returns 1
;; or `tree` is a pair, in which case `vertices`returns an exact positive integer
;; Looking up path-condition tails `γ₁` and `γ₂` recursively tell facts
;; about `(car tree)` and `(cdr tree)`

;; By massaging things, we can infer the type
;; vertices : (μ (X) (U Number (Pairof X X))) → Exact-Positive-Integer

((1 @ 1) ‖ ((number? tree)))

((●_exact-positive-integer?
  @
  (+ (+ 1 (vertices (car tree))) (vertices (cdr tree))))
 ‖
 ((cons? tree) (not (number? tree)) γ₁ γ₂))

;;;;; error cases

((blame
    "/var/tmp/scv_strawman_14788134281478813428461.rkt"
    car
    (cons?)
    (|●_(λ (𝒙) (not (number? 𝒙)))|))
   ‖
   ((cons? tree) (not (number? tree)) γ₀))

((blame
    "/var/tmp/scv_strawman_14788134281478813428461.rkt"
    car
    (cons?)
    (|●_(λ (𝒙) (not (number? 𝒙)))|))
   ‖
   ((not (cons? tree)) (not (number? tree))))

((blame
    "/var/tmp/scv_strawman_14788134281478813428461.rkt"
    car
    (cons?)
    (|●_(λ (𝒙) (not (number? 𝒙)))|))
   ‖
   ((cons? tree) (not (number? tree)) γ₃ γ₂))