Michael Norrish
Michael Norrish
I think it's pretty clear that the Basis library says this should be a signed infinity value. ``` - 3.0 / 0.0; ! Uncaught exception: ! Div ```
McAfee on my corporate windows test machine sees the download as `Artemis!909EB37BCC9E`
I am perhaps not providing enough mount-style options, but when I try ``` sudo apfs-fuse -d 255 /dev/sda2 /mnt/macdrive ``` I get back ``` Device /dev/sda2 opened. Size is 1500092153856...
See, this from the Isabelle mailing list > It is possible that this formalisation is not faithful to the IEEE standard. The commit message of the changeset that is to...
In the following, `valueOf` extracts a value from a monad (`'a M -> 'a`). This is possible, for example, in a writer monad. In something like the option monad, you'd...
In things like `cardeq_TRANS`, there's an extra type variable that gets turned into an ugly genvarified blob when you use `irule` or `irule_at`. Often, the desired type is clear; there...
The Reference manual used to include a big list of the core system's theorems. I found this useful when I was learning HOL, so perhaps we should try to do...
A conditional rewrite theorem of the form P a b ==> f a = g b is usually useless to the simplifier and ignored as a result. However, it could...
Holmake reports the error but tells the user it occurs at the end of the file. It would be much more helpful if it reported the location of the unmatched...
E.g.: ``` ``(GENLIST (++) n = GENLIST f) n``; Exception- HOL_ERR {message = "on line 3, characters 10-13:\nCouldn't infer type for overloaded name ++", origin_function = "type-analysis", origin_structure = "Preterm"}...