## Stream: lean4

### Topic: AssocList "failed to synthesize"

#### Zygimantas Straznickas (Jan 09 2021 at 23:09):

import Std.Data.AssocList

def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
#eval l -- works
#eval (List.toAssocList l) -- failed to synthesize Lean.Eval (Std.AssocList Nat Nat)


possible bug?

#### Mario Carneiro (Jan 09 2021 at 23:15):

I would guess that Lean.Eval means something like lean 3's has_repr, a way to print the resulting data structure

#### Mario Carneiro (Jan 09 2021 at 23:16):

In other words, while lean can compute the AssocList, it doesn't know how to show the result

#### Bryan Gin-ge Chen (Jan 10 2021 at 00:11):

This was a fun little exercise:

import Std.Data.AssocList

def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
#eval l -- works

def Std.AssocList.ToList : AssocList α β → List (α × β)
| AssocList.nil => []
| AssocList.cons k v t => (k, v) :: ToList t

instance [Repr α] [Repr β] : Repr (Std.AssocList α β) where
reprPrec f _ := repr f.ToList

#eval (l.toAssocList) -- works


#### Zygimantas Straznickas (Jan 10 2021 at 00:13):

Thanks! I'm coming from Coq so my knowledge of Lean 3 is limited :) Is there a way to just see the fully reduced term? I tried #reduce (in Lean 4) but in this example it gives me

Std.AssocList.cons 1 1
{ fst :=
List.rec
{ fst :=
(fun (t : List (Nat × Nat)) (f : List.below t) =>
(match t with
| [] => fun (x : List.below []) => Std.AssocList.nil
| (a, b) :: es => fun (x : List.below ((a, b) :: es)) => Std.AssocList.cons a b x.fst.fst)
f)
[] PUnit.unit,
snd := PUnit.unit }
(fun (head : Nat × Nat) (tail : List (Nat × Nat))
(v_0 : PProd ((fun (x : List (Nat × Nat)) => Std.AssocList Nat Nat) tail) (List.below tail)) =>
{ fst :=
(fun (t : List (Nat × Nat)) (f : List.below t) =>
(match t with
| [] => fun (x : List.below []) => Std.AssocList.nil
| (a, b) :: es => fun (x : List.below ((a, b) :: es)) => Std.AssocList.cons a b x.fst.fst)
f)
(head :: tail) { fst := v_0, snd := PUnit.unit },
snd := { fst := v_0, snd := PUnit.unit } })
[(2, 2)],
snd := PUnit.unit }.fst.fst


instead of the expected cons 1 1 (cons 2 2 nil)

#### Zygimantas Straznickas (Jan 10 2021 at 00:14):

hmm, #reduce fully reduces this in Lean 3

#### Mario Carneiro (Jan 10 2021 at 12:14):

It appears that lean 4 #reduce isn't actually full reduction, it is just doing whnf

#### Mario Carneiro (Jan 10 2021 at 12:15):

if you peel off the top level constructor it will continue to make progress

Last updated: May 18 2021 at 23:14 UTC