このまえも出てきたpartialの証明 本に書いてあることをコードで書くとこうなります > (J-Bob/prove (my/prelude) '(((defun partial (x) (if (partial x) 'nil 't)) (size x) ((Q) (natp/size x)) (() (if-true (if (< (size x) (size x)) 't 'nil) 'nil)))…