Derive for inductive types with non-type parameters #286

Activity

1. annenkov commented on May 12, 2022

   

   annenkov

   on May 12, 2022

   Author

   More actions

   I think something like this could be generated (just by changing the case when d is a type):

     fun (d : D) (mu9_ : Show (Address d)) =>
       {|
         show := fun x : msg =>
                   let
                     fix aux (x' : msg) : string :=
                     match x' with
                     | send p0 => "send " ++ smart_paren (show p0)
                     end in
                   aux x |}.
   

   👍React with 👍1Reacted by Xia Li-yao
2. Lysxia

   added

   enhancement

   on May 12, 2022
3. liyishuai

   added

   part:derive

   on Jun 8, 2023