Idris supports both modes of interaction, although the set of available tactics is not yet as useful as that of Coq.
Idris sprijină ambele moduri de interacțiune, deși setul de tactici disponibile nu este încă la fel de util ca cel al Coq.