+ _
+ adj_sndOfNotNil
+ coeMLList
+ cons_getVert
+ cons_getVert_succ
+ cons_sndOfNotNil
+ exists'
+ ext_iff'
+ filter_subset'
+ getVert_one
+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ mem_getLast?_append_of_mem_getLast?
+ mem_head?_append_of_mem_head?
+ ofMLList
+ sndOfNotNil
+ tail_support_eq_support_tail
+ toLazyList
+-+- empty_toList
- AddContent.ext_iff
- Bornology.ext_iff
- MeasurableSpace.ext_iff
- Nodup.erase
- Nodup.erase_eq_filter
- Nodup.mem_erase_iff
- Nodup.not_mem_erase
- Nodup.sublist
- Perm.ext_iff
- Sublist.map
- TransGen
- _root_.Acc.TransGen
- _root_.WellFounded.transGen
- _root_.acc_transGen_iff
- adj_getVert_one
- and_forall_succ
- attach_eq_nil
- attach_map_val
- attach_nil
- countP_attach
- count_attach
- drop
- enumFrom_append
- enumFrom_cons'
- enumFrom_eq_nil
- enumFrom_eq_zip_range'
- enumFrom_map
- enumFrom_map_snd
- enumFrom_singleton
- enum_append
- enum_cons'
- enum_eq_nil
- enum_eq_zip_range
- enum_map
- enum_map_snd
- enum_singleton
- eq_iff
- exists_eq_right'
- exists_or_eq_left
- exists_or_eq_left'
- exists_or_eq_right
- exists_or_eq_right'
- exists_prop_congr
- exists_prop_of_true
- exists_true_left
- ext_dual_iff
- ext_inner_iff
- filter_subset
- foldl_join
- foldr_join
- forall_mem_ne
- fst_lt_add_of_mem_enumFrom
- fst_lt_of_mem_enum
- gcd_def
- get!_none
- get!_some
- get?_pmap
- getElem?_enum
- getElem?_enumFrom
- getElem?_pmap
- getElem?_zipWith'
- getElem?_zipWith_eq_some
- getElem?_zip_eq_some
- getElem_enum
- getElem_enumFrom
- getElem_eq_getElem?
- getElem_pmap
- getElem_zip
- getElem_zipWith
- getLast?_append
- getLast_cons
- getLast_pmap
- getLast_reverse
- getVert_cons
- getVert_cons_one
- getVert_cons_succ
- getVert_copy
- get_pmap
- head?_append
- head_mem
- head_replicate
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- isSome_map
- join_append
- join_concat
- join_join
- join_reverse
- le_fst_of_mem_enumFrom
- length_attach
- length_filter_lt_length_iff_exists
- length_join
- length_pmap
- limit_ext_iff
- lt_length_left_of_zip
- lt_length_left_of_zipWith
- lt_length_right_of_zip
- lt_length_right_of_zipWith
- map_eq_map_iff
- map_fst_add_enumFrom_eq_enumFrom
- map_fst_add_enum_eq_enumFrom
- map_pmap
- map_prod_left_eq_zip
- map_prod_right_eq_zip
- mem_attach
- mem_enumFrom
- mem_pmap
- mem_zip
- ne_nil_of_length_pos
- nodup_cons
- nodup_iota
- nodup_nil
- nodup_range
- nodup_range'
- nodup_replicate
- not_nil_iff_lt_length
- or_exists_succ
- pairwise_gt_iota
- pairwise_le_range
- pairwise_lt_range
- pairwise_lt_range'
- pi_ext'_iff
- pmap_append
- pmap_append'
- pmap_congr
- pmap_eq_map
- pmap_eq_map_attach
- pmap_eq_nil
- pmap_map
- range'_one
- reverse_eq_iff
- reverse_join
- snd_mem_of_mem_enum
- snd_mem_of_mem_enumFrom
- sublist_replicate_iff
- support_tail_of_not_nil
- tail_cons_eq
- tail_cons_nil
- takeWhile_cons_of_neg
- takeWhile_cons_of_pos
- take_range
- unique_ext_iff
- unzip_enumFrom_eq_prod
- unzip_enum_eq_prod
- unzip_eq_map
- unzip_left
- unzip_right
- unzip_zip
- unzip_zip_left
- unzip_zip_right
- zipWith_comm
- zipWith_comm_of_comm
- zipWith_distrib_reverse
- zipWith_same
- zip_of_prod
- zip_unzip
- «forall»
-+-+ Hom.ext'
-+-+- ext
-- subtype_ext_iff
-- «exists»
--- ext_ring_iff
------------------------------------------------------------------------------------------------------------ ext_iff

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.