The example in example.v could be expressed with better notation than the current draft. Here is a start of the notation that should be introduced for the final submission:
Let ldl_norm_infty n := ldl_fun (fun (t : (n.+1).-tuple R) => [tuple \big[maxr/[tnth t 0] ]_(i <- t) i ])%R.
Notation "`|| t ||" := (ldl_lookup (ldl_norm_infty t) 0).
Notation "t `! n" := (ldl_lookup _ t n) (at level 55).
The example in
example.vcould be expressed with better notation than the current draft. Here is a start of the notation that should be introduced for the final submission: