Add nicer names in derive.param2

[proux01]

n1, n2 and n_R are more readable than H, H0 and H1

[proux01]

From elpi.apps Require Import derive.std.

Elpi derive.param2 list.
Print list_R. (*                                                                                                                                                                          
* before                                                                                                                                                                                  
Inductive list_R (A A0 : Type) (A1 : A -> A0 -> Type) : list A -> list A0 -> Type :=                                                                                                      
  | nil_R : list_R A A0 A1 nil nil                                                                                                                                                        
  | cons_R : forall (H : A) (H0 : A0), A1 H H0 ->                                                                                                                                         
             forall (H1 : list A) (H2 : list A0), list_R A A0 A1 H1 H2 ->                                                                                                                 
             list_R A A0 A1 (H :: H1) (H0 :: H2).                                                                                                                                         
Arguments list_R (A A)%type_scope A%function_scope (s1 s2)%list_scope                                                                                                                     
Arguments nil_R (A A)%type_scope A%function_scope                                                                                                                                         
Arguments cons_R (A A)%type_scope A%function_scope _ _ _ (_ _)%list_scope _                                                                                                               
                                                                                                                                                                                          
* after                                                                                                                                                                                   
Inductive list_R (A1 A2 : Type) (A_R : A1 -> A2 -> Type) : list A1 -> list A2 -> Type :=                                                                                                  
  | nil_R : list_R A1 A2 A_R nil nil                                                                                                                                                      
  | cons_R : forall (a1 : A1) (a2 : A2), A_R a1 a2 ->                                                                                                                                     
             forall (l1 : list A1) (l2 : list A2), list_R A1 A2 A_R l1 l2 ->                                                                                                              
             list_R A1 A2 A_R (a1 :: l1) (a2 :: l2).                                                                                                                                      
Arguments list_R (A1 A2)%type_scope A_R%function_scope (s1 s2)%list_scope                                                                                                                 
Arguments nil_R (A1 A2)%type_scope A_R%function_scope                                                                                                                                     
Arguments cons_R (A1 A2)%type_scope A_R%function_scope a1 a2 a_R (l1 l2)%list_scope l_R                                                                                                   
*)

Definition fa (n : nat) (b : bool) := 0.

Elpi derive.param2 fa.
Print fa_R. (*                                                                                                                                                                            
* before                                                                                                                                                                                  
fa_R = fun (n n0 : nat) (_ : nat_R n n0) (b b0 : bool) (_ : bool_R b b0) => O_R                                                                                                           
Arguments fa_R (n n)%nat_scope n (b b)%bool_scope b                                                                                                                                       
                                                                                                                                                                                          
* after                                                                                                                                                                                   
fa_R = fun (n1 n2 : nat) (_ : nat_R n1 n2) (b1 b2 : bool) (_ : bool_R b1 b2) => O_R                                                                                                       
Arguments fa_R (n1 n2)%nat_scope n_R (b1 b2)%bool_scope b_R                                                                                                                               
*)

[proux01]

Thanks