I would like to define function by induction "Calculate" ,that takes a Term (that could be a Name, Variable or a Pair) and return a Nat.
Ex. Calculate of Name is 0
Calculate of Var is 0
Calculate of Pair(m,n) is Calculate (m) + Calculate (n)
Somthing similar to the Fibonacci function. Should I use Recdef or Inductive? if I have to use Recdef how I should map the Term (like: measure function λn. n in Fibonacci)?
Thanks for any advice