The Coq mailing list

[Ly Kim Quyen <lykimq AT gmail.com>]

Hi,

...

Definition rules := list rule.

Definition trs := rules.

Definition trsInput := trs -> option strategy -> option (rules) -> option (rules).

In another file I defined these functions: 

Where 

arity_in_term : term -> symbol -> option nat

arity_in_list

     : forall A : Type,

       (A -> symbol -> option nat) -> list A -> symbol -> option nat

arity_in_rule

     : rule -> symbol -> option nat

Definition arity_in_rules rs f := arity_in_list arity_in_rule rs f.

Definition arity_in_trs (rs: trs) f := arity_in_rules rs f.

I defined a function arity_in_trs if I do not give the type for parameter 'rs' it will return for me a type (list rule). Because I want it return for me a type 'trs'. So I give it a type (rs: trs) and Coq combine and recognized its type. 

In another function: 

Definition arity_in_trsInput (t: trsInput) f := arity_in_trs t f. 

I got an problem. I want the return type of arity_in_trsInput : trsInput -> symbol -> option nat. 

My question is: 

- why I can pass the combine in the first function "arity_in_trs" and 

- in another function "arity_in_trsInput" it need an trsInput type, so how can I define it?

Thank you very much,