Zulip Chat Archive

Stream: lean4

Topic: Boolean and/or etc

Kevin Buzzard (Oct 19 2022 at 17:20):

I see that lean 4 has booleans, but I couldn't find the definition of Boolean and and or either in core or std4. They were in core in Lean 3. Did I miss them or shall I define them in mathlib4? (I'm porting a Boolean file)

Henrik Böving (Oct 19 2022 at 17:21):

It is simply called and and or in the top level, defined in Init/Prelude.lean

David Renshaw (Oct 19 2022 at 17:22):

https://github.com/leanprover/lean4/blob/e44fd19074259018b9ddcbdb00209492416bc8ac/src/Init/Prelude.lean#L958-L972

David Renshaw (Oct 19 2022 at 17:22):

(I located that source location by visiting https://leanprover-community.github.io/mathlib4_docs/index.html )

Kevin Buzzard (Oct 19 2022 at 17:24):

Thanks both. Oh that link to mathlib4_docs is super-helpful!

Henrik Böving (Oct 19 2022 at 17:24):

docs4#and and docs4#or work as well by the way^^

Adam Topaz (Oct 19 2022 at 17:47):

And we also have the "standard" programmer notation for these:

example (b : Bool) : Bool := !b
example (a b : Bool) : Bool := a && b
example (a b : Bool) : Bool := a || b

Matthew Ballard (Oct 19 2022 at 18:06):

Henrik Böving said:

docs4#and and docs4#or work as well by the way^^

Should these lead to blank pages?

Adam Topaz (Oct 19 2022 at 18:06):

They work for me

Matthew Ballard (Oct 19 2022 at 18:07):

Hmm.

Adam Topaz (Oct 19 2022 at 18:07):

Here is the direct link: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#or

Matthew Ballard (Oct 19 2022 at 18:08):

I've been having the blank page issue with docs4 links for a bit and curious if it is just me (Safari, MacOS).

Adam Topaz (Oct 19 2022 at 18:08):

Do the Lean3 docs links work for you? docs#and

Matthew Ballard (Oct 19 2022 at 18:11):

Yes

Adam Topaz (Oct 19 2022 at 18:15):

Firefox gives me a warning in the console about a missing <!DOCTYPE html> in the docs4 page. I wonder if that's the issue?

Matthew Ballard (Oct 19 2022 at 18:16):

Firefox renders it fine. It's a Safari issue.

Adam Topaz (Oct 19 2022 at 18:17):

yeah what I mean is that Safari might be more strict about requiring <!DOCTYPE html>

Matthew Ballard (Oct 19 2022 at 18:24):

https://leanprover-community.github.io/mathlib4_docs/ renders ok in Safari.

Matthew Ballard (Oct 19 2022 at 18:26):

I also accumulate more / after mathlib4_docs/ in the url as I click around

Mauricio Collares (Oct 19 2022 at 18:41):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/doc-gen4.20feature.20request/near/290542810 probably (TL;DR: Safari does not support certain regex features which are used in docgen search)

Henrik Böving (Oct 19 2022 at 18:45):

Matthew Ballard said:

I also accumulate more / after mathlib4_docs/ in the url as I click around

That is a usual thing...I invested a little time into investigating why but i eventually stopped since its a basically irrelevant UX bug and I got other stuff to do and on top of that don't actually know what I'm doing with web development :D if someone wants to PR a fix for that feel free.

Marcus Rossel (Oct 20 2022 at 06:53):

Matthew Ballard said:

I've been having the blank page issue with docs4 links for a bit and curious if it is just me (Safari, MacOS).

I'm experiencing exactly the same issues as you. And the issues are also present with Safari on iOS.

Ruben Van de Velde (Oct 20 2022 at 08:07):

The issue seems to be that WebKit doesn't support these regexes:

const LEAN_FRIENDLY_AND_SEPARATOR = /(?<!«[^»]*)&/;
const LEAN_FRIENDLY_EQUAL_SEPARATOR = /(?<!«[^»]*)=/;
const LEAN_FRIENDLY_SLASH_SEPARATOR = /(?<!«[^»]*)\//;

with "SyntaxError: Invalid regular expression: invalid group specifier name"

Mario Carneiro (Oct 20 2022 at 08:08):

is there a way to do something which is slightly less featureful on webkit?

Mario Carneiro (Oct 20 2022 at 08:09):

The use there seems to be avoiding & inside of name quotations but let's just say that's an unlikely input to a search (seeing as it's fairly hard to even type «)

Mario Carneiro (Oct 20 2022 at 08:13):

something like

const LEAN_FRIENDLY_AND_SEPARATOR = try /(?<!«[^»]*)&/ catch _ => /&/;

except in javascript syntax

Ruben Van de Velde (Oct 20 2022 at 08:28):

Submitted https://github.com/leanprover/doc-gen4/pull/85

Henrik Böving (Oct 20 2022 at 18:16):

Does it work on Mac now?

Matthew Ballard (Oct 20 2022 at 18:17):

Yes. Thanks.

Last updated: Dec 20 2023 at 11:08 UTC