You could write
HD ([]:’a list) = @x:’a. T
or, equivalently, HD [] = ARB.
Michael
From: "buday.gerg...@uni-eszterhazy.hu"
Date: Friday, 15 February 2019 at 15:34
To: hol-info , "Norrish, Michael (Data61,
Acton)"
Subject: Re: [Hol-info] 0 / 0 = 0 ???
Is HD [] at all possible to define?
Is HD [] at all possible to define? For some fixed list type yes but in general
for [] : 'a list ?
- Gergely
Az Android Outlook letöltése
On Fri, Feb 15, 2019 at 12:00 AM +0100, wrote:
The author of LENGTH_TL probably didn’t have access to the updated
Sorry for my previous confusing email, this is something I didn't know
about. It seems now TL and TL_T are the same.
Jeremy
On 02/15/2019 09:59 AM, michael.norr...@data61.csiro.au wrote:
> the updated definition of TL.
___
hol-info mailing list
It's a deliberate choice. See the discussion in Section 1.2 of
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf
On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
wrote:
> Hi,
>
> in HOL's realTheory, division is defined
Hi,
in HOL's realTheory, division is defined by multiplication:
[real_div] Definition
⊢ ∀x y. x / y = x * y⁻¹
and zero multiplies any other real number equals to zero, which is
definitely true:
[REAL_MUL_LZERO] Theorem
⊢ ∀x. 0 * x = 0
However, above two theorems together
