algorithmic typing and conversion up to completeness of conv #338
kyoDralliam
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
Annotations
1 error and 3 warnings
|
build:
theories/Decidability/Functions.v#L76
Non exhaustive pattern-matching: no clause found for pattern tId _ _ _
|
|
build
Argument B was previously inferred to be in scope type_scope but is
|
|
build
Argument B was previously inferred to be in scope type_scope but is
|
|
build
Argument B was previously inferred to be in the empty scope stack
|