creating lists

Stream: new members

[Holly Liu]

for def l := list(1 × bool), what is the error failed to synthesize type class instance for has_one (Type ?) ?

[Eric Wieser]

You're asking for it to for the type of lists of elements of type prod (1 : Type*) bool, and lean is telling you "I don't know what type 1 is".

[Eric Wieser]

Were you trying to say "lists of length 1"?

[Holly Liu]

oh i was trying to make a list consisting of only (1 x tt) and (1 x ff). how would i do this?

[Eric Wieser]

Do you mean (1, tt) and (1, ff)?

[Holly Liu]

oh right

[Eric Wieser]

What do you mean by 1 there? Do you mean 1 as a nat? 1 as an int? 1 as the only element of unit?

[Holly Liu]

i think 1 as nat

[Adam Topaz]

I think #xy will help here...

[Kevin Buzzard]

i.e. "what are you actually doing"?

[Eric Wieser]

list ({n : nat // n = 1} × bool) is the literal translation of what you asked for, but it's unlikely that's actually a good idea

[Kyle Miller]

This is probably to do with free group words (I'm guessing you're using nat for the generators?) Here's how you make a list of (1, tt) and (1, ff):
def l := [(1, tt), (1, ff)]

[Holly Liu]

yes, i was trying to get the length of the list by doing something like for def braid3 := [(1, tt), (1, ff)], try#eval braid3.length (sorry for the late reply, i was away from my laptop for all of last week)

[Holly Liu]

Kyle Miller said:

using nat for the generators?

yes i think this is what we're doing, unless a different type might be better when using the presented groups method to define braids.