deriving iterator

Stream: metaprogramming / tactics

[Alok Singh]

Or ForIn or whatever the typeclass is called. inspired by https://docs.rs/derive_more/latest/derive_more. i want to tag an (iterable) field of my structure and use that as the underlying iterator.

structure LeviCivita where
  -- I want this as the  underlying iterator for `LeviCivita`
  coeffs : HashMap Rat Rat

[Alok Singh]

@Kyle Miller ?

[Yury G. Kudryashov]

What should it derive?

[Yury G. Kudryashov]

Could you make a non-working #mwe that shows what you expect to write and what definition/instance you want to have autogenerated?

[Kyle Miller]

The expectation would be that if c : LeviCivita then for x in c do ... would be equivalent to for x in c.coeffs do ....

[Kyle Miller]

There's also ForIn' for the version you get membership proofs per iteration, but here's how you can copy a ForIn instance:

import Lean

open Lean

set_option autoImplicit true

structure A where
  xs : List Nat

instance : ForIn m A Nat where
  forIn a b f := forIn a.xs b f

[Kyle Miller]

Seems like it wouldn't be too hard to make a command that derives ForIn and ForIn' from a field.