On Fri, Apr 26, 2013 at 4:50 PM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Sure. I don't know what was the original reason for allowing two
> variables of different types to have the same name but I always found
> this extremely weird.
> I guess maybe this makes the logic easier to express in some way,
> because otherwise we need mappings from variable names to types (called
> "environments").
> But I'm not convinced myself by this argument since we need environments
> in other contexts anyway (probably in the semantics).
>
Where would these environments live in the implementation of the logic?
Are they attached to terms?
Then something like:
let x = mk_var("P",bool) in
let P = mk_var("P",`:bool->bool`) in
mk_comb(P,x)
would have to either fail or automatically rename a variable.
This could be annoying in writing automation when the variables come from
elsewhere (not just calls to mk_var).
> Note that having an environment (i.e., a mapping from variable names to
> types) is what is done in Coq for instance.
>
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
