Zulip Chat Archive

Stream: maths

Topic: Friday afternoon puzzle -- 37 ∈ 37?


view this post on Zulip Kevin Buzzard (Nov 20 2020 at 15:46):

At Xena yesterday I was too quick with my use of use, accidentally using 37 for a set of reals. But it worked! Shing noted that set \R now has zero, one and add, so numerals work. This reminds me a bit of ZFC, where the corresponding result is false. Puzzle: is it true in Lean?

import tactic

namespace foo

-- all these work fine
instance : has_zero (set ) := by apply_instance
instance : has_one (set ) := by apply_instance
instance : has_add (set ) := by apply_instance
-- so numerals work too

end foo

example :  (a : ) (b : set ), a  b :=
begin
  use 37,
  use 37,
  -- ⊢ 37 ∈ 37
  sorry
end

view this post on Zulip Gabriel Ebner (Nov 20 2020 at 15:51):

docs#set.singleton_one also looks scarily non-well-founded.

view this post on Zulip Reid Barton (Nov 20 2020 at 15:53):

Maybe it would make sense to put basically this whole file in a locale?

view this post on Zulip Reid Barton (Nov 20 2020 at 15:53):

e.g. open_locale pointwise to get these instances

view this post on Zulip Eric Wieser (Nov 20 2020 at 15:55):

lemma silly (n : ) : n  (n : set ) :=
begin
  induction n,
  simp,
  rw nat.succ_eq_add_one,
  apply set.add_mem_add,
  convert n_ih,
  exact set.one_mem_one,
end

example :  (a : ) (b : set ), a  b :=
begin
  use 37,
  use 37,
  convert silly 37,
  simp,
end

view this post on Zulip Damiano Testa (Nov 20 2020 at 15:55):

Also, tidy proves it...

view this post on Zulip Damiano Testa (Nov 20 2020 at 15:56):

here is the proof tidy finds:

use 37,
use 37,
fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, refl } } }, refl } } }, refl },

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 15:56):

In ZFC, 37 ∈ 38...

view this post on Zulip Damiano Testa (Nov 20 2020 at 15:57):

or, without following the misleading second use:

example :  (a : ) (b : set ), a  b := 37, _, by solve_by_elim

view this post on Zulip Sebastien Gouezel (Nov 20 2020 at 15:57):

example (n : ) : n  (n : set ) :=
begin
  induction n with n hn ih,
  { simp only [nat.cast_zero, set.mem_zero] },
  { exact n, 1, by simpa using hn⟩,}
end

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 15:58):

I didn't really expect anything beyond entertainment to come from this post, but actually maybe Reid has a point. I remember @Mario Carneiro being a bit concerned about defining addition on set A too (A something with +)

view this post on Zulip Johan Commelin (Nov 20 2020 at 16:04):

lemma mem_bit0 [has_add α] {s : set α} {a : α} (h : a  s) : bit0 a  bit0 s :=
a, a, h, h, rfl

lemma mem_bit1 [has_one α] [has_add α] {s : set α} {a : α} (h : a  s) : bit1 a  bit1 s :=
bit0 a, 1, mem_bit0 h, one_mem_one, rfl

example :  (a : ) (b : set ), a  b :=
begin
  use [37, 37],
  solve_by_elim only [mem_bit1, mem_bit0, one_mem_one, zero_mem_zero] {max_depth := 6}
end

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:07):

example :  (a : ) (b : set ), a  b := 37, _, rfl

(practicing minimizing skills)

view this post on Zulip Johan Commelin (Nov 20 2020 at 16:07):

I just wanted to post that one

view this post on Zulip Johan Commelin (Nov 20 2020 at 16:07):

@Damiano Testa Yeah, you're getting scary

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 16:08):

spoiler alert:

example (n : ) : (n : set ) = {n} :=
begin
  induction n with n hn,
  { exact set.singleton_zero },
  simp [hn],
end

view this post on Zulip Bryan Gin-ge Chen (Nov 20 2020 at 16:31):

Amusing as this is, I agree with Reid that the pointwise instances on set should be hidden in a locale.

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 16:34):

IIRC Mario's objection was that one could imagine a scenario where one has a local definition of addition on subsets of X (e.g. when making them a boolean ring, when you might want + to mean xor), and then you'd have problems if X accidentally also had an addition.

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:43):

With a view towards further developments, the boolean structure on subsets often shows up in explicit representations of 2-torsion points on hyperelliptic curves. In such cases, the underlying set X could very well be a field. Would that be an issue?

view this post on Zulip Damiano Testa (Nov 20 2020 at 16:44):

(in the example of hyperelliptic curves, the 2-torsion points might be subsets of ramification points, or rather 2-set partitions of the ramification points)

view this post on Zulip Eric Wieser (Nov 20 2020 at 16:48):

If we end up not moving these, should we add @Johan Commelin's bit0 lemmas as norm_cast?

view this post on Zulip Gabriel Ebner (Nov 20 2020 at 17:08):

Johann's lemmas do not mention coe, so they can't be norm_cast. But an version should be simp.

view this post on Zulip Damiano Testa (Nov 20 2020 at 17:17):

To add to the silliness of the Friday afternoon: @Johan Commelin 's first lemma can be proved as follows:

lemma mem_bit0 [has_add α] {s : set α} {a : α} (h : a  s) : bit0 a  bit0 s :=
begin
  repeat { fconstructor, exact _›, },
  fconstructor,
end

For me, it is the first time that fconstructor closes a goal, I think.

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 17:42):

See if you can get split to close a goal :-)

view this post on Zulip Damiano Testa (Nov 20 2020 at 17:47):

Ahaha! I was wondering whether I was more surprised by fconstructor or split and went for fconstructor!

view this post on Zulip Johan Commelin (Nov 20 2020 at 17:50):

Gabriel Ebner said:

Johann's lemmas do not mention coe, so they can't be norm_cast. But an version should be simp.

Sadly, the iff version isn't true. For example bit0 2 \mem bit0 {1,3}

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 18:56):

I'd never really internalised this {1}=1 thing but I was just working on valuations this evening and proving lemmas about trivial valuations. I noticed this was missing:

lemma subgroup.closure_eq_bot_iff (G : Type*) [group G] (S : set G) :
  closure S =   S  {1} :=
begin
  sorry
end

so I tried simp and it changed the RHS to S ⊆ 1. Meh :-/

view this post on Zulip Mario Carneiro (Nov 20 2020 at 20:33):

I was surprised to see that 0 = {0} in that definition. I would have guessed 0 = empty

view this post on Zulip Mario Carneiro (Nov 20 2020 at 20:34):

which for me is enough to suggest that these should not be simp normal form, because they are not universal enough

view this post on Zulip Mario Carneiro (Nov 20 2020 at 20:36):

as for 1 : set A I just have no idea what that should mean. It could mean univ if you treat set A as a boolean algebra and notate the top and bottom with 0 and 1. (We don't, but some books do and this would be a source of confusion)

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:35):

Sorry for beating to death this thread, but I got hung up on the tidy proof and while trying to make sense of it, I realized that Lean either subtracts 1 or divides by 2, when the number is even (see below). Why is that?

example :  (a : ) (b : set ), a  b :=
begin
  refine 37, 37, _⟩,
  refine 36, 1, _⟩⟩,  --here Lean subtracts 1
  rw [eq_self_iff_true, and_true, set.mem_one, eq_self_iff_true, and_true],
  refine 18, 18, _⟩⟩,  --here Lean divides by 2
  rw [eq_self_iff_true, and_true, and_self],
  refine 9, 9, _⟩⟩,
  rw [eq_self_iff_true, and_true, and_self],
  refine 8, 1, _⟩⟩,
  rw [eq_self_iff_true, and_true, set.mem_one, eq_self_iff_true, and_true],
  refine 4, 4, _⟩⟩,
  rw [eq_self_iff_true, and_true, and_self],
  refine 2, 2, _⟩⟩,
  rw [eq_self_iff_true, and_true, and_self],
  refine 1, 1, _⟩⟩,
  rw [eq_self_iff_true, and_true, and_self],
  exact set.mem_one.mpr rfl,
end

I would have imagined that Lean would have subtracted 1 all the way.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:37):

set_option pp.numerals false

#check 37 -- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℕ

Lean stores numerals internally as binary.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:38):

Ah! So this proof is a more clunky version of Johan's, right? Thanks for the explanation!

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:39):

Btw, Lean tells me

#check 37  -- 37 : ℕ

I do not see the binaries...

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:39):

example : 1000000000 + 1000000000 = 2000000000 := rfl -- works
example : 1000000 + 2000000 = 3000000 := rfl -- times out

I was surprised the first time I saw this.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:40):

Damiano Testa said:

Btw, Lean tells me

#check 37  -- 37 : ℕ

I do not see the binaries...

That's because you didn't do what I did.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:41):

Sorry, I missed the first line of your code... :face_palm:

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:41):

The pp. options just control what the pretty printer outputs (the infoview).

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:41):

The elaborator turns 37 into some internal representation, and the pretty printer turns it back into the 37.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:42):

Thanks for the explanation!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:44):

I think that at some point in my Lean education someone told me about set_option pp.all true, which means "print out what Lean is really thinking", and the realisation that I could do this suddenly taught me a lot about what was going on internally. Sometimes you think "Lean why are you so slow", but then when you turn on pp.all you discover that it is manipulating gigantic terms.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:45):

set_option pp.all true

example : 37 = 37 :=
begin
  sorry
end

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:45):

I had a similar realization when I found out about show_term and started using it on all the lines of my code!

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:45):

I will explore set_option pp.all true now!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:45):

Try it in the middle of a commutative algebra proof and you might get a bit of a shock!

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:47):

Already I can see that I no longer have to guess how many _ I have to use in a refine ⟨_, _, ...⟩ expression!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:47):

PS re pp.all -- the infoview actually makes things a bit worse here. In the old days when we just had text output, the pp.alloutput was really nicely formatted.

set_option pp.all true

example : 37 = 37 :=
begin

end

The error here has really nice spacing (especially if you make the infoview window big).

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:49):

This set_option really seems to clarify lots of things that were obscure in the "digested" view on the right

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:50):

Try #help options .

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:50):

I now need to look back at all the code that I wrote, turning this on!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:51):

Those give you all the options you can play with. I have never used 95% of them :-) Many are just for people debugging Lean.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:51):

Kevin Buzzard said:

Try #help options .

This means that I can do set_option and then any one of the things that this outputs, right?

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:51):

Kevin Buzzard said:

Those give you all the options you can play with. I have never used 95% of them :-) Many are just for people debugging Lean.

Ok, thanks!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:51):

Right. But for the mathematician end user, most of these are not helpful.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:52):

Things like pp.all help a huge amount when you can't close x = x with rfl though. You can find out yourself exactly what went wrong.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:53):

If you see that one side has an _inst_1 in and the other side an _inst_5 that's when you realise that you have two abelian group structures on something.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:53):

Yes, I can see exactly where this would have helped with the order_dual stuff

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:54):

When lean is computing max and I have no idea if it means max or min!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:54):

Oh yeah, then you would have been able to see exactly what was going on. I'm sorry I didn't look at that issue more carefully.

view this post on Zulip Damiano Testa (Nov 21 2020 at 09:55):

Do not worry: this way I used alone convert refl _ for the first time!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:56):

My feeling is that this sort of thing might be solved best by making stuff irreducible. But I didn't think too carefully. If order_dual X = X then that's fine, but then if some tactic manages to actually _change_ order_dual X back to X then that's when you're in trouble.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 09:59):

When I was working with valuations and groups with 0, we would be working with with_zero X and sometimes this would magically change to option X because with_zero X is defined to be option X but of course you want it to always stay as with_zero X to remind both you and Lean that it's X{0}X\cup\{0\} rather than XX plus some arbitrary extra thing. But sometimes a tactic like simp might change with_zero X to option X and suddenly things are confusing (especially if you are also using with_bot or with_top or whatever). I fixed this by making with_zero irreducible and then things were much better, but also a bunch of proofs broke so I had to fix them :-)

view this post on Zulip Damiano Testa (Nov 21 2020 at 10:01):

When I will have some time, I will look into irreducible: what you describe seems very relevant!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 10:01):

But once we'd got things working again, stuff was better because Lean wasn't doing this incorrect unfolding.

def order_dual (α : Type*) := α

This definition is fine, but the problem is that when later on Lean is trying to guess what a type is, the elaborator might guess wrong, and think you mean alpha instead of order_dual alpha. Because they are definitionally equal, an order_dual X might accidentally turn back into an X and now all of a sudden max = min and things become impossible to work with. Marking order_dual irreducible will stop this happening.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 10:04):

import tactic

#print order_dual -- def order_dual :

#print with_zero -- @[irreducible] def with_zero : ...

order_dual isn't irreducible. It was only relatively recently we realised that this sort of thing could really help. The reals weren't irreducible for a while, and then occasionally Lean would think "I know, let's consider this real as an equivalence class of Cauchy sequences of rationals", which is 100% never what you want to do. Probably more things should be irreducible -- it guides Lean in the right direction.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 10:06):

The idea is that you make the definition, make the API with it not irreducible (so e.g. you can prove transitivity of < on order_dual X from transitivity of > on X) and then make it irreducible at the end of the file. Then in other files making API, you temporarily make it semireducible so you can do these tricks again if you need them.

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 10:07):

But end users shouldn't be needing to unfold it, they should have all the lemmas they need from the API, and should be imagining order_dual X as in some sense being a completely different object to X -- even the map from X to order_dual X should have a name which isn't id.

view this post on Zulip Damiano Testa (Nov 21 2020 at 10:07):

Ok, I am not at the computer right now, but will look into this as soon as I am! Thanks!

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 10:07):

(because id won't work any more if order_dual is irreducible). This is the price you pay, but it makes you write more principled code.

view this post on Zulip Damiano Testa (Nov 21 2020 at 10:08):

Yes, what you describe is very close to what I experienced!

view this post on Zulip Patrick Massot (Nov 21 2020 at 11:38):

Damiano, note that pp.all is much less needed now that we have info view widgets. The advantage of widgets is you can choose what to display instead of getting overwhelmed by pp.all. If you don't understand what I mean then you can post a #mwe where you feel pp.all helps you and I'll explain how to get the same information from widgets.

view this post on Zulip Mario Carneiro (Nov 21 2020 at 11:51):

I think it's easier to do diffing on a type mismatch with pp.all than with the goal view

view this post on Zulip Mario Carneiro (Nov 21 2020 at 11:52):

it's also easier to post a pp.all expression in zulip

view this post on Zulip Mario Carneiro (Nov 21 2020 at 11:52):

particularly if you don't know what you are looking for

view this post on Zulip Kenny Lau (Nov 21 2020 at 12:10):

import algebra.pointwise

example :  (a : ) (b : set ), a  b :=
begin
  refine 37, 37, _⟩,
  have h1 : 1  (1 : set ) := rfl,
  have h2 : 2  (2 : set ) := 1, 1, h1, h1, rfl⟩,
  have h4 : 4  (4 : set ) := 2, 2, h2, h2, rfl⟩,
  have h8 : 8  (8 : set ) := 4, 4, h4, h4, rfl⟩,
  have h9 : 9  (9 : set ) := 8, 1, h8, h1, rfl⟩,
  have h18 : 18  (18 : set ) := 9, 9, h9, h9, rfl⟩,
  have h36 : 36  (36 : set ) := 18, 18, h18, h18, rfl⟩,
  have h37 : 37  (37 : set ) := 36, 1, h36, h1, rfl⟩,
  exact h37
end

view this post on Zulip Kenny Lau (Nov 21 2020 at 14:19):

import algebra.pointwise

example :  (a : ) (b : set ), a  b :=
begin
  refine 37, 37, _⟩,
  simp_rw [bit1, bit0,  set.singleton_one, set.singleton_add_singleton, set.mem_singleton]
end

view this post on Zulip Kenny Lau (Nov 21 2020 at 14:20):

import algebra.pointwise

meta def foo : tactic unit :=
`[{apply set.add_mem_add; foo} <|> exact set.one_mem_one]

example :  (a : ) (b : set ), a  b :=
begin
  refine 37, 37, _⟩,
  foo
end

view this post on Zulip Riccardo Brasca (Nov 21 2020 at 15:27):

Sorry for the silly questions, but what are widgets?

view this post on Zulip Riccardo Brasca (Nov 21 2020 at 15:32):

Also... does 37 ∈ 37 mean that sets in lean are not well founded or am I missing something obvious?

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 15:34):

It's not 37 ∈ 37, it's 37 ∈ \uparrow 37, right?

view this post on Zulip Reid Barton (Nov 21 2020 at 15:35):

The two :37: s mean different things

view this post on Zulip Riccardo Brasca (Nov 21 2020 at 15:35):

Ah OK, that's reassuring :D

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 15:51):

Any type which has a 0, a 1 and an + automatically gets a 37. In this case this was unintentional, and the joke was to work out what this set actually was. Turns out it's {37}.

view this post on Zulip Riccardo Brasca (Nov 21 2020 at 15:55):

I see, set ℕ is a monoid with 1, it makes sense.

view this post on Zulip Alex J. Best (Nov 21 2020 at 19:52):

Riccardo Brasca said:

Sorry for the silly questions, but what are widgets?

Widgets are a way of viewing arbitrary html in the goal view due to @Edward Ayers. In vscode this is what allows us to click terms in the goal view and repeatedly click on subterms and go to definition, and gives the nice highlighting of subterms.


Last updated: May 10 2021 at 07:15 UTC