]>
matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
[ list_empty ⇒ 𝟎
| list_lcons l q ⇒
match l with
- [ label_d _ ⇒ depth q
+ [ label_d k ⇒ depth q
| label_m ⇒ depth q
| label_L ⇒ ↑(depth q)
| label_A ⇒ depth q