Re: [isabelle] Trying to fit HOL to traditional math verbiage
The function type operator (the "=>" we were using
before) is primitive, that is, not created by type definition. In the
usual model of HOL in set theory, it constructs function spaces.
Makes sense, I guess. And even in src/ZF/ZF.thy I see that primitive.
It's all functional programming. That's my revelation of yesterday.
Anything that gives me recursion is probably going to be functional
My requirements have changed. All I want is the easiest possible way to
learn a tool that allows me to do some logic and have the appearance of
sets. If there's a problem, it's false illusions.
This archive was generated by a fusion of
Pipermail (Mailman edition) and