Vincent,
Thanks for your input on this. Are there some examples in HOL or HOL Light
where the approach you suggest with option types is used? (Preferably some
elementary theory where I won't get too lost as a non-mathematician.) This
is unfamiliar to me except of course in the programming languag
Konrad,
Yes, your example with MOD and DIV I think is just the right sort of thing.
It's still annoying to
know that the result of dividing by zero is some number, but not as bad as
having a definite but unexpected result, and the issue is less obtrusive
this way, too.
I presume that the same so
Petros, your consider code is a huge step toward what I need. I'll try to
finish modifying your code tonight. Here's the string version I have now, and
below that is an earlier term version:
let consider vars_t prfs lab =
let len = String.length vars_t in
let rec findSuchThat = function
Thanks, Vincent! I definitely have to work your exercise now. Two dumb
questions:
1) how do I get quotexpander to turn off type inference by putting a period at
the end of the terms? Of all your possibilities, that's the one I like best.
2)Doesn't Ocaml use the "applicative order application
Dear Lockwood,
First, thank you for taking the time to try out HOL-Omega. You are a
pioneer!
Yes, you are correct in all you are reporting about the examples in the
HOL-Omega Tutorial, that they work correctly for interactive use, but will
fail when inserted directly, without modification, into a
In my opinion, the best way of dealing with this is to use option types: None
denoting the undefined value. This makes function composition tedious but you
can use a monad to make this easier.
Now, it is not standard w.r.t. usual maths. But I'm not sure whether usual
maths are doing this the ri
Partial functions are annoying, no matter how you approach them.
One way to introduce a partial operation in HOL is with
new_specification. In contrast with new_definition, this allows
you to introduce a constant with only its relevant properties.
Consider, for example, the so-called division algo
I have had HOL Omega installed, asking that the instructions of Section 1.3 of
the HOL Omega System Tutorial be followed (what I am unfortunately too ignorant
to attempt myself), and have been working my way through the Tutorial with
great interest, Holmake-ing the example theories as I go. All
Dear HOL experts,
I am hoping for wisdom and recommendations from you all related to a
question I have. Let me start with a bit of background information, which
is here largely to orient you to my understanding of the situation. I know
the facts are elementary.
Usually in mathematics some operat
On 04/04/2013 03:55, Bill Richter wrote:
> Petros, I have some understanding now of your X_MATCH_CHOOSE_TAC: the
> variable x' doesn't need a type annotation that X_CHOOSE_TAC would need,
> because it infers the type from the existential statement xth by
> xtm = concl xth
> x,bod = dest_exists
10 matches
Mail list logo
