notation < "| T |" with precedence 25 for @{'abs $T}.
interpretation "Fsub named type length" 'abs T = (nt_len T).
interpretation "list length" 'abs l = (length ? l).
notation < "| T |" with precedence 25 for @{'abs $T}.
interpretation "Fsub named type length" 'abs T = (nt_len T).
interpretation "list length" 'abs l = (length ? l).
interpretation "natural swap" 'swap a b n = (swap a b n).
interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T).
interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T).
interpretation "natural swap" 'swap a b n = (swap a b n).
interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T).
interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T).