CAP_project icon indicating copy to clipboard operation
CAP_project copied to clipboard

Published 20 hours ago • verified publisher icon homalg-project

Introduce IsSafeWellDefinedFor* or IsMathematicallyWellDefinedFor*

Open mohamed-barakat opened this issue 6 months ago • 1 comments

The current IsWellDefinedForObjects and IsWellDefinedForMorphism include tests for checking whether the type of ObjectDatum/MorphismDatum is correct. They all compile to true.

It would make sense to introduce IsSafeWellDefinedFor* or IsMathematicallyWellDefinedFor* which assumes that these type-check-tests are true and only tests the "mathematical" conditions. Only the latter should be compiled and are relevant in the proof-assistant mode.

mohamed-barakat avatar Aug 10 '24 20:08 mohamed-barakat