In dafny language, we have a map datatype:

datatype MapSet $=$ MapSet $($s : map$)$

How would I go about coding the function below?

function size $($m:MapSet$)$: int

$\{$

$/*$ return the size of the map $($m$)$ where only the keys with the boolean value "true" are counted $*/$

$\}$

Note: In dafny, for loops are not usable for functions, but this problem has to stay a function.