doc-src/Tutorial/Datatype/tsubst
changeset 5851 15ce4c1c8313
equal deleted inserted replaced
5850:9712294e60b9 5851:15ce4c1c8313
       
     1 primrec
       
     2   "subst s (Var x) = s x"
       
     3   "subst s (App f ts) = App f (substs s ts)"