[Agda] Type Checking in Agda

[Ashish Mishra]

Hi All,

Can any one elaborate the Type Checking(and inference ) Algorithm used by
Agda, provide or some pointers for the same. I am interested in the Type
Checking of dependent types and since Agda has full support of "dependent
types", i assume It will be helpful looking at that.
Moreover , since the Typability of dependent type theory is undecidable in
general( correct me if i am wrong here ), what approximations Agda uses to
get a decidable type checker.

Thanks



-- 
Regards,
Ashish Mishra
Graduate Student,
Computer Science and Automation Department,IISc
Cell : +91-9611194714
Mailto : ashishmishra at csa.iisc.ernet.in
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151027/f62b968f/attachment.html