lean4-htt/src/Std/Data/HashMap
Markus Himmel 92cca5ed1b
chore: remove bif from hash map lemmas (#4791)
The original idea was to use `bif` in computation contexts and `if` in
propositional contexts, but this turned out to be really inconvenient in
practice.
2024-07-22 14:39:00 +00:00
..
AdditionalOperations.lean feat: Std.HashMap (#4583) 2024-07-05 10:14:20 +00:00
Basic.lean doc: mention linearity in hash map docstring (#4771) 2024-07-17 09:26:38 +00:00
Lemmas.lean chore: remove bif from hash map lemmas (#4791) 2024-07-22 14:39:00 +00:00
Raw.lean doc: mention linearity in hash map docstring (#4771) 2024-07-17 09:26:38 +00:00
RawLemmas.lean chore: remove bif from hash map lemmas (#4791) 2024-07-22 14:39:00 +00:00