Commit 2024-11-30 09:42 ba7312b5

View on Github →

chore: move definition of ENat and PNat out of Order.TypeTags (#19485) These had been moved to Order.TypeTags to reduce imports elsewhere, but they are sort of off-topic here, so I've just moved them to their own files.

Estimated changes

added def ENat.recTopCoe
added theorem ENat.recTopCoe_coe
added theorem ENat.recTopCoe_top
added def ENat
added def PNat.val
added def PNat
deleted def ENat.recTopCoe
deleted theorem ENat.recTopCoe_coe
deleted theorem ENat.recTopCoe_top
deleted def ENat
deleted def PNat.val
deleted def PNat