# [isabelle] unhelpful comment in Term.ML

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] unhelpful comment in Term.ML
*From*: Michael Norrish <Michael.Norrish at nicta.com.au>
*Date*: Tue, 10 Nov 2015 23:25:53 +0000
*Accept-language*: en-US, en-AU
*Thread-index*: AQHRHA8knTEnAQ1oPkK49kq0JR8qDw==
*Thread-topic*: 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.*