Singly-linked list/Element definition: Difference between revisions
Content added Content deleted
m (→{{header|ATS}}) |
|||
Line 314: | Line 314: | ||
dataviewtype rclist_vt (vt : vt@ype+, n : int) = |
dataviewtype rclist_vt (vt : vt@ype+, n : int) = |
||
| rclist_vt_nil (vt, 0) |
| rclist_vt_nil (vt, 0) |
||
| {0 <= n} rclist_vt_cons (vt, n + 1) of (vt, rclist_vt (vt, n)) |
| {0 <= n} rclist_vt_cons (vt, n + 1) of (vt, rclist_vt (vt, n)) |
||
(* An axiom one will need: lists never have negative lengths. *) |
|||
extern praxi {vt : vt@ype} |
|||
rclist_vt_param {n : int} |
|||
(lst : !rclist_vt (vt, n)) :<prf> |
|||
[0 <= n] void</lang> |
|||
=={{header|AutoHotkey}}== |
=={{header|AutoHotkey}}== |