First properties of reducibility (induction, escape, reflexivity) #346
Annotations
1 error and 3 warnings
build:
theories/Decidability/Functions.v#L80
Non exhaustive pattern-matching: no clause found for pattern tW _ _
|
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
|