Lars just informed me that I didn't actually include an example in my
mail (I thought I did); it was therefore probably not clear what I meant
exactly, so let me explain:
When I write "\ci" in a theory, it used to be completed to ∘
immediately. As of 1ca11ddfcc70, this does not happen
This particular issue has, in fact, annoyed me a great deal. I needed
the ‘dist_norm’ lemma a lot lately and was never able to find it with
‘find_theorems’, which was very frustrating. I eventually found it by
reading a proof that used it somewhere.
I did not think much of it at the time, but
As of the following revision, immediate completion does not work anymore
in Isabelle/JEdit:
changeset: 61600:1ca11ddfcc70
user:wenzelm
date:Sat Nov 07 16:05:28 2015 +0100
summary: clarified completion of explicit symbols (see also
f6bd97a587b7, e0e4ac981cf1);
From the
Ah, interesting. Thanks!
On 23/09/15 08:47, Andreas Lochbihler wrote:
> Dear Manuel,
>
> consider supports the same syntax as obtains, i.e., you can use "where"
> as in
>
> consider "x = ∞" | "x = -∞" | y where "x = ereal y&quo
On 27/06/15 09:06, Florian Haftmann wrote:
What about: »a = unit_factor a * normalize a«
Sounds reasonable.
I still had the hope that it would be possible to develop an abstract
specification for gcd which would form a lattice: »gcd a a = a«. But
now I cam to realize that for Gcd :: 'a set =
Hallo,
thanks for all the good work. It's nice to finally see my work
integrated so neatly into HOL.
1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on
On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit to
determine the type of an expression such as “of_nat k”, as there is nothing to
click on.
When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it
says ‘constant
.
declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)
Today the output says sqrt (real_of_nat 2). But if there would be no
abbreviation for of_nat :: nat ⇒ real, how would you deduce the type
of the coercion.
Dmitriy
On 24.06.2015 16:01, Manuel Eberl wrote:
On 24/06/15 15:55, Larry
I also vote for b). I would also like to add that I ran into situations
where I required the notation of an inverse element in a ring. I defined
this as ring_inv x = 1 div x. For instance, on int, we have ring_inv
1 = 1 and ring_inv (-1) = -1 and everything else is basically
ill-defined, because 1
I think the main (and only) problem is that it uses significantly more
memory.
On 28/05/15 11:21, Peter Lammich wrote:
Hi list,
When I start Isabelle, I get the following warning message on the
console:
### Cannot execute Poly/ML in 32bit mode (missing shared libraries for
C/C++)
### Using
I am not terribly happy about that. I use approximation of powr in my work on
Akra–Bazzi and the Master theorem.
I take it that a powr b = exp (ln a * b) still holds for positive a. I could
probably apply that rewrite rule before applying approximation, but it would of
course be nice if I did
Yes, but the underlying reason for that is that complex numbers are
isomorphic to pairs of real numbers, and binary product types are
degenerate (I would rather say very basic) co-algebraic datatypes.
So my point (and I would guess Andrei's as well) is that this really has
nothing to do with
types are “natural” codatatypes, so defining
them as datatypes makes everything a bit more clumsy.
Cheers,
Manuel Eberl
On 07.05.2014 16:50, Makarius wrote:
On Wed, 7 May 2014, Johannes Hölzl wrote:
* Theorems about complex numbers are now stated only using Re and Im,
the Complex
constructor
Hallo,
I am not, as it were, a user of Proof General anymore; however, I would
like, if I may, to point out one thing that annoys me in jEdit and that
was, in my opinion, better in Proof General: the handling of
abbreviations for Unicode characters.
The current behaviour with “immediate
Hallo,
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context - term - thm -- is that not an
ML interface to the Fun_Cases tool? Or do you also want a
Hallo,
partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is
an abbreviation for 'a ⇒ 'b option. There is syntax such as [1 ↦ 2, 3 ↦
4], meaning, basically, λx. if x = 1 then Some 2 else if x = 3 then
Some 4 else None. There is also update syntax for such function, such
as f(1 ↦
Be that as it may, even in that case, I would like the code export tool
to at least output a warning or an error message. Having the code export
tool export produce faulty Haskell code can hardly be intended behaviour.
As an analogy: when I give invalid code to a compiler, I expect it to
complain
Hallo,
I just noticed that when exporting code to Haskell, there is a
complication when some of the theories involved have lower-case names.
The code export itself will work with no error or warning, but when
ghc/ghci are invoked on the generated code, they will report the
lower-case module name
101 - 118 of 118 matches
Mail list logo
