-definition lref_map:
- ((nat \to nat)) \to (nat \to (T \to T))
-\def
- let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t
-with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match
+rec definition lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match
+t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match