AgdaVsCoq-Talk

• About that interactiveness point: in my experience coq proofs can be very interactive when done with proof general or coqide. --opqdonut
• for implicit arguments, Agda is not really more "light-weight" as Coq also supports {} (implicit) declarations instead of () (explici)
• Someone should add that coq seems more 'clunky' when writing dependently typed programs. For example; there is no way to un-import all the builtin stuff like nat.

-- Well, there is still the 'nois' option in Coq to have a session with only built-ins ('nat' is not a Coq built-in), so you can un-import it. What you cannot do though is un-import something already imported.

• I don't understand the "Induction-recursion" point. Coq does allow mutual inductive types/mutually structural recursive functions (using the 'with' connective keyword between two Inductive or Fixpoint definitions); this is covered in section 14.3/p400 of Coq'Art. Would appreciate clarification. :-)

-- Induction-recursion is the mutual definition of an inductive type *and* a recursive function taking an inhabitant of this type as an argument