]>
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
[ list_empty ⇒ 𝟎
| list_lcons l q ⇒
match l with
| label_m ⇒ depth q
| label_L ⇒ ↑(depth q)
| label_A ⇒ depth q
| label_m ⇒ depth q
| label_L ⇒ ↑(depth q)
| label_A ⇒ depth q