3 ms·
Did you consider using dependent types to define the image database in such a way that it's impossible to create one that's not InternallyConsistent? This appro
by logicchains 9y ago
Did you consider using dependent types to define the image database in such a way that it's impossible to create one that's not InternallyConsistent? This approach can often make proofs shorter/simpler.
- reuben364 9y agoCoq isn't very good for developing with properties encoded in the types. Such properties are defined seperately from the data structures involved.