How did Lean infer an algorithm for list.perm?

Stream: new members

[Huỳnh Trần Khanh]

the definition of list.perm doesn't resemble an algorithm at all, it's "inductively defined", not sure if this is the right term. so how can Lean infer an algorithm and run it when I #reduce the list.perm predicate?

[Huỳnh Trần Khanh]

i mean #eval sorry

[Huỳnh Trần Khanh]

(deleted)

[Huỳnh Trần Khanh]

this doesn't look like an algorithm does it https://github.com/leanprover-community/mathlib/blob/5360e476391508e092b5a1e5210bd0ed22dc0755/src/data/list/perm.lean#L24

[Horatiu Cheval]

You define something as a bool. So, Lean automatically applies to_bool to list.perm which normally returns a Prop, as can be seen by #print something. In turn, to_bool needs a decidable Prop, and this decidability provides in some sense, an algorithm

[Horatiu Cheval]

This is just my guess

[Horatiu Cheval]

In particular, docs#list.decidable_perm would be that algorithm

[Horatiu Cheval]

You can see list.decidable_perm appearing in #print something by first setting set_option pp.implicit true