projects / tatoo.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 31d4549) | patch
Add two functions to the Node_list interface (and to the naive implementation):
authorKim Nguyễn <kn@lri.fr>
Tue, 13 May 2014 12:36:20 +0000 (14:36 +0200)
committerKim Nguyễn <kn@lri.fr>
Tue, 13 May 2014 12:40:36 +0000 (14:40 +0200)
commitcfbd6490c8b03b820375f79ff4d009ed2d0252c3
tree8b7d413f49b6b948a57cdd292694573d9ff17de7tree | snapshot
parent31d45495fda9a110fd348f8b492761c28b434ec9commit | diff
Add two functions to the Node_list interface (and to the naive implementation):
* pop discards the first element
* append appends the element of the second argument at the end of the first one (in place).
src/naive_node_list.ml diff | blob | history
src/node_list.ml diff | blob | history
Tree Automata TOOlkit