# [isabelle] Interpreting lists as an instance of monoid_mult fails

```Hello,

```
I am trying to use the fact that lists form a monoid to obtain some algebraic properties of lists for free.
```However, I run into the following complaint, which I do not understand:

```
Partially applied constant "List.append" on left hand side of equation, in theorem:
```monoid_mult.prod_list [] (@) ?xs ≡ foldr (@) ?xs []
```
```
The minimal theory featuring the problem is here:

```
```theory ListMonoid

imports Main

begin

interpretation semilist: semigroup_mult append
proof-
show "class.semigroup_mult (@)"
proof
show "⋀a b c. (a @ b) @ c = a @ (b @ c)"
by simp
qed
qed

interpretation monlist: monoid_mult "[]" "(@)"
proof-
show "class.monoid_mult [] (@)"
proof
show "⋀a. [] @ a = a"
by simp
next
show "⋀a. a @ [] = a"
by simp
qed
qed

end
```
```
I am using Isabelle2018/HOL with jEdit.

```
I should add that I am aware of the following existing interpretations of list's "append"
```
```
```interpretation semilist: semigroup append

interpretation monolist: monoid  append Nil
```
```
```
The reason why I needed the context monoid_mult is that I wanted to use the results of the theory HOL/Power.thy
```
```
Is there any way how to fix this? (Obviously, it does not take too much effort to just prove all useful facts afresh, but I wanted to understand what is going on).
```
Best regards

Stepan Holub

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.