
 0 | module Syntax.IHateParens.Fin
 1 | 
 2 | import public Data.Fin
 3 | 
 4 | %default total
 5 | 
 6 | public export %inline
 7 | (.asNat) : Fin n -> Nat
 8 | (.asNat) = finToNat
 9 |