Singly-linked list/Element definition: Difference between revisions
Singly-linked list/Element definition (view source)
Revision as of 23:40, 20 March 2022
, 2 years ago→{{header|ATS}}
m (→{{header|ATS}}) |
|||
Line 314:
dataviewtype rclist_vt (vt : vt@ype+, n : int) =
| rclist_vt_nil (vt, 0)
| {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}}==
| |||