lean4-htt/src/Std
Rob23oba acfc9c50d5
feat: hash map lemmas for filter, map and filterMap (#7400)
This PR adds lemmas for the `filter`, `map` and `filterMap` functions of
the hash map.

---------

Co-authored-by: jt0202 <johannes.tantow@gmail.com>
Co-authored-by: Johannes Tantow <44068763+jt0202@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
2025-04-17 10:15:52 +00:00
..
Classes chore: adjust BEq classes (#7855) 2025-04-16 13:24:23 +00:00
Data feat: hash map lemmas for filter, map and filterMap (#7400) 2025-04-17 10:15:52 +00:00
Internal chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00
Net feat: add network interfaces (#7578) 2025-03-24 17:57:05 +00:00
Sat chore: upstream Nat material from mathlib (#7971) 2025-04-16 06:55:32 +00:00
Sync refactor: more complete channel implementation for Std.Channel (#7819) 2025-04-12 21:02:24 +00:00
Tactic feat: make bv_decide work on simp normal forms of shifts (#7976) 2025-04-15 17:26:19 +00:00
Time chore: upstream Int lemmas from mathlib (#7983) 2025-04-16 17:45:08 +00:00
Classes.lean feat: tree map data structures and operations (#6914) 2025-02-11 14:47:47 +00:00
Data.lean feat: tree map data structures and operations (#6914) 2025-02-11 14:47:47 +00:00
Internal.lean feat: implement basic async IO with timers (#6505) 2025-01-13 18:11:04 +00:00
Net.lean feat: Std.Net.Addr (#6563) 2025-01-09 09:33:03 +00:00
Sat.lean feat: Std.Sat.AIG (#4953) 2024-08-12 14:58:38 +00:00
Sync.lean feat: add Std.SharedMutex (#7770) 2025-04-03 08:30:54 +00:00
Tactic.lean chore: fix spelling mistakes in src/Std/ (#5431) 2024-09-23 20:39:34 +00:00
Time.lean chore: fix spelling mistakes (#7328) 2025-04-07 01:15:48 +00:00