Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

dependent types in Lisp (Idris BTFO)

Name: Anonymous 2018-12-17 1:29

;;--------------------------------------------------------------------
;;-- Types

;; slot-number type
(defun within-slot-number-rangep (n)
(not (or (< n 0) (> n 255))))

(deftype slot-number ()
`(and fixnum (satisfies within-slot-number-rangep)))

;; vitality type
(defun within-vitality-rangep (v)
(not (or (< v -1) (> v 65535))))

(deftype vitality ()
`(and fixnum (satisfies within-vitality-rangep)))

;; field type
(deftype field ()
`(or fixnum function))

(deftype field-application ()
`(and function))

;;--------------------------------------------------------------------
;;-- Structures

;; slot structure
(defstruct slot
(number 0 :type index)
(field #'identity :type field)
(vitality 10000 :type vitality))

Name: Anonymous 2018-12-18 23:43

>>2
did you not see DEFTYPE?

Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List