search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
77 stars 18 forks source link

derive doesn't work in mutual blocks #43

Closed locallycompact closed 2 years ago

locallycompact commented 2 years ago 
mutual

  record A where
    constructor MkA
    foo : B

  record B where
    constructor MkB
    bar : Maybe A

  %runElab derive "A" [Generic, Meta, Eq, Show]
  %runElab derive "B" [Generic, Meta, Eq, Show]

results in

Error: While processing right hand side of implEqA. Can't find an implementation for POP_ Type Eq [[B]].
stefan-hoeck commented 2 years ago

There's deriveMutual for that.

locallycompact commented 2 years ago

Much obliged