[isabelle] unhelpful comment in Term.ML



The comment is

(*Substitute arguments for loose bound variables.
  Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
  Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
        and the appropriate call is  subst_bounds([b,a], c) .
  Loose bound variables >=n are reduced by "n" to
     compensate for the disappearance of lambdas.
*)

The behaviour is to substitute the first term in the list for Bound 0, the second for Bound 1, etc.  This doesn't seem to be what the second line of the comment is implying.

Behaviour is visible in

ML {*
  Term.subst_bounds ([ at {term "x::'a"}, @{term "f::'a => 'b"}], Bound 0 $ Bound 1)
*}

which gives x $ f, rather than f $ x.

Michael

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.