@@ -32,8 +32,8 @@ pub trait LocallyCoherentLineageStore<M: MathsCore, H: Habitat<M>>:
3232{
3333 #[ must_use]
3434 #[ debug_requires(
35- habitat. contains ( indexed_location. location ( ) ) ,
36- "indexed location is inside habitat "
35+ habitat. is_indexed_location_habitable ( indexed_location) ,
36+ "indexed location is habitable "
3737 ) ]
3838 fn get_global_lineage_reference_at_indexed_location (
3939 & self ,
@@ -42,8 +42,8 @@ pub trait LocallyCoherentLineageStore<M: MathsCore, H: Habitat<M>>:
4242 ) -> Option < & GlobalLineageReference > ;
4343
4444 #[ debug_requires(
45- habitat. contains ( lineage. indexed_location. location ( ) ) ,
46- "indexed location is inside habitat "
45+ habitat. is_indexed_location_habitable ( & lineage. indexed_location) ,
46+ "indexed location is habitable "
4747 ) ]
4848 #[ debug_ensures( self . get_lineage_for_local_reference(
4949 & ret
@@ -68,9 +68,10 @@ pub trait LocallyCoherentLineageStore<M: MathsCore, H: Habitat<M>>:
6868 #[ debug_requires( self . get_lineage_for_local_reference(
6969 & reference
7070 ) . is_some( ) , "lineage is active" ) ]
71- #[ debug_ensures( old( habitat) . contains(
72- ret. indexed_location. location( )
73- ) , "prior location is inside habitat" ) ]
71+ #[ debug_ensures(
72+ old( habitat) . is_indexed_location_habitable( & ret. indexed_location) ,
73+ "prior indexed location is habitable"
74+ ) ]
7475 #[ debug_ensures( self . get_lineage_for_local_reference(
7576 & old( unsafe { crate :: cogs:: Backup :: backup_unchecked( & reference) } )
7677 ) . is_none( ) , "lineage was deactivated" ) ]
@@ -104,7 +105,10 @@ pub trait GloballyCoherentLineageStore<M: MathsCore, H: Habitat<M>>:
104105 fn iter_active_locations ( & self , habitat : & H ) -> Self :: LocationIterator < ' _ > ;
105106
106107 #[ must_use]
107- #[ debug_requires( habitat. contains( location) , "location is inside habitat" ) ]
108+ #[ debug_requires(
109+ habitat. is_location_habitable( location) ,
110+ "location is habitable"
111+ ) ]
108112 fn get_local_lineage_references_at_location_unordered (
109113 & self ,
110114 location : & Location ,
0 commit comments