Error Index

` | b | c | e | i | n | r | s | t | u | ‘


	`
	`qualid` is not a module

	b
	`bad occurrence number of ‘qualid’`

	c
	`Cannot handle mutually (co)inductive records.`
	`Cannot infer a term for this placeholder.`
	`Cannot use mutual definition with well-founded recursion or measure`

	e
	`Either there is a type incompatibility or the problem involves dependencies`

	i
	`Impossible to unify … with …`

	n
	`No argument name ‘ident’`
	`No such label ‘ident’`
	`Non exhaustive pattern-matching`
	`Not the right number of missing arguments`

	r
	`Records declared with the keyword Record or Structure cannot be recursive.`

	s
	`Signature components for label ‘ident’ do not match`
	`Statement without assumptions`

	t
	`The constructor ‘ident’ expects ‘num’ arguments`
	`The elimination predicate term should be of arity ‘num’ (for non dependent case) or ‘num’ (for dependent case)`
	`The recursive argument must be specified`
	`This is not the last opened module`
	`This is not the last opened module type`
	`This is not the last opened section`

	u
	`Unable to apply`
	`Unable to find an instance for the variables ‘ident’…‘ident’`
	`Unable to infer a match predicate`
	`Undeclared universe ‘ident’.`
	`Universe inconsistency.`

	‘
	`‘qualid’ does not denote an evaluable constant`
	`‘qualid’ does not occur`