# IRC log for #isabelle, 2017-02-06

All times shown according to UTC.

Time Nick Message
10:56 silver joined #isabelle
11:30 juls joined #isabelle
12:23 mal`` joined #isabelle
18:06 chindy joined #isabelle
18:06 julian_ joined #isabelle
18:07 chindy can someone explain why i get the error no type arity list, and what it means? http://pastebin.com/MwWaUUJC
18:08 pruvisto chindy: look at "term fold"
18:09 pruvisto it first takes the list to fold over and then the initial state
18:09 pruvisto the way you wrote it, "A" would be the initial state and "0" would be the list to fold over
18:10 pruvisto since "0" must be a list and 0 is defined in the type class "zero", the type checker infers that "list" must be an instance of the type class "zero"
18:10 pruvisto which it isn't, hence the error message
18:11 pruvisto Also, you shouldn't use "≡" on the right-hand side.
18:11 pruvisto ≡  is a meta-logical thing that you rarely have to use directly
18:11 pruvisto (e.g. when defining abbreviations)
18:11 pruvisto it returns a "prop", not a "bool", so you get another type error there
18:11 pruvisto you want to write "tst A B ≡ (fold (op+) A 0 = fold (op+) B 0)"
18:12 pruvisto or, arguably better, "tst A B = (fold (op+) A 0 = fold (op+) B 0)"
18:12 pruvisto or, my favourite, "tst A B ⟷ fold (op+) A 0 = fold (op+) B 0"
18:12 chindy oh... dont know why i had the wrong argument order ...
18:12 pruvisto (⟷ is just an abbreviation for equality of Booleans, but with weaker precedence)
18:13 pruvisto (so it mixes well with equality)
18:13 pruvisto (and other Boolean connectives like ∧ and ∨)
18:14 pruvisto (e.g. "foo = A ∨ B" is parsed as "(foo = A) ∨ B", but "foo ⟷ A ∨ B" is parsed as "foo = (A ∨ B)")
18:49 chindy i kind of have difficulties understanding how the lambda/eta operators work on vectors (theory Analysis) so if i want a vector of type R^2 with values 1.0 , 2.0 with one it would be (χ i. 1.0) and with 2 ?
19:45 pruvisto chindy: something like (χi. if i = 0 then 1 else if i = 1 then 2 else undefined)
19:45 pruvisto or just (χi. if i = 0 then 1 else 2)
19:48 pruvisto don't know if there's a nice way
19:48 pruvisto I've never used vectors myself
19:49 pruvisto depending on what you want to do exactly, it might be easier to use "real × real" instead of "real ^ 2"
19:49 pruvisto (which is "(real, 2) vec")
21:54 logicmoo joined #isabelle
23:27 mbrcknl_ joined #isabelle