[Agda] Type inference

[Nils Anders Danielsson]

On 2009-09-29 15:22, Robin Green wrote:
> Why can Agda not infer all types in Test.agda (attached), while it can
> for Test2.agda?

The types can be inferred if you use a less general variant of <_,_>:

  <_,_> : {A B : Set} {C : B → Set}
          (f : A → B) → ((x : A) → C (f x)) → (A → Σ B C)
  < f , g > x = (f x , g x)

The variant in the standard library has the following type:

  <_,_> : {A : Set} {B : A → Set} {C : ∀ {x} → B x → Set}
          (f : (x : A) → B x) → ((x : A) → C (f x)) →
          ((x : A) → Σ (B x) C)
  < f , g > x = (f x , g x)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.