|
Agda.TypeChecking.Implicit |
|
|
Description |
Functions for inserting implicit arguments at the right places.
|
|
Synopsis |
|
|
|
Documentation |
|
|
Constructors | ImpInsert Int | this many implicits have to be inserted
| BadImplicits | hidden argument where there should have been a non-hidden arg
| NoSuchName String | bad named argument
| NoInsertNeeded | |
|
|
|
|
|
|
The list should be non-empty.
|
|
Produced by Haddock version 2.6.1 |