feat: expand mapping functionailty in core - #1857

Open

LiamSchilling wants to merge 8 commits into

opencompl:mainfrom

LiamSchilling:maps

Commits on Nov 11, 2025

feat: `fromMap'` as alternative to `map'` for `HVector`
LiamSchilling
committed
6c7b8f7
feat: define `castMap` to take the role of previous `map' f fun _ => id`
LiamSchilling
committed
32714ee
fix: bind variables in hypotheses to `castMap` impicitly for easier resolution
LiamSchilling
committed
1d0f3f5
feat: define `toMap` for mapping valuations between mapped contexts
LiamSchilling
committed
65fae7f
fix: prefix `toMap` with namespace `Valuation`
LiamSchilling
committed
e8ac3ab
feat: define `castToMap` to take the role of previous `toMap fun _ => id`
LiamSchilling
committed
4db3056
feat: prove application lemmas for `Valuation` maps
LiamSchilling
committed
724fd2b
feat: abbreviate element-wise types and maps for regions
LiamSchilling
committed
ce86b8a