Commit 6c7d3b97fcf58d3240a10f96f660fee437be74dc
1 parent
216a520c
add to_DB_id, which convert an Int into DB_id type
Showing
1 changed file
with
12 additions
and
0 deletions
Show diff stats
database/db_types.anubis
| @@ -67,6 +67,18 @@ public define Int | @@ -67,6 +67,18 @@ public define Int | ||
| 67 | none then (Int)-1, | 67 | none then (Int)-1, |
| 68 | db_id(_idx) then _idx | 68 | db_id(_idx) then _idx |
| 69 | }. | 69 | }. |
| 70 | + | ||
| 71 | +public define DB_id | ||
| 72 | + to_DB_id | ||
| 73 | + ( | ||
| 74 | + Int value | ||
| 75 | + )= | ||
| 76 | + if value < 0 then | ||
| 77 | + none | ||
| 78 | + else | ||
| 79 | + db_id(value) | ||
| 80 | +. | ||
| 81 | + | ||
| 70 | 82 | ||
| 71 | public define String | 83 | public define String |
| 72 | to_String | 84 | to_String |