Commit graph

13 commits

Author SHA1 Message Date
Kim Morrison
c25d206647
chore: Fin.ofNat' uses NeZero (#5356) 2024-09-16 07:13:18 +00:00
François G. Dorais
759ece7f9e
fix: naming convention for UInt lemmas (#4514)
Closes #4513

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
2024-08-12 01:03:21 +00:00
Markus Himmel
3e0ea762b8
feat: Std.HashMap (#4583)
### Preliminary PRs:

- [x] #4597 
- [x] #4599
- [x] #4600
- [x] #4602
- [x] #4603
- [x] #4604
- [x] #4605
- [x] #4607
- [x] #4627
- [x] #4629 

### Quick overview over API/naming changes compared to `Lean.HashMap`
and `Batteries.HashMap`:
#### Lean

* `find?` -> `get?`/`getElem?`
* `find!` -> `get!`/`gtetElem!`
* `findD` -> `getD`
* `findEntry?` -> not implemented for now
* `insert'` -> `containsThenInsert` (order reversed in result)
* `insertIfNew` -> `getThenInsertIfNew?` (order reversed in result)
* `numBuckets` -> `Internal.numBuckets`
* `ofListWith` -> not implemented for now
* `Array.groupByKey` -> not implemented for now
* `merge` -> not implemented for now, but you can use `insertMany`

#### Batteries

* `modify` -> not implemented for now
* `mergeWith` -> not implemented for now
* `mergeWithM` -> not implemented for now
2024-07-05 10:14:20 +00:00
Markus Himmel
a2a73e9611
feat: USize.and_toNat (#4629)
Split from #4583
2024-07-03 01:28:36 +00:00
Markus Himmel
4055aecba2
feat: additional lemmas for bounded integers (#4605)
Split from #4583
2024-07-02 02:03:13 +00:00
Leonardo de Moura
8c03650359
feat: some Char, UInt, and Fin theorems (#4231)
for SSFT24 summer school: https://github.com/david-christiansen/ssft24

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
2024-05-21 06:11:23 +00:00
Mario Carneiro
5eb274d486
fix: don't use modulo for UInt upcasting (#3960)
This makes `(v : UInt8).toUInt16.toNat = (v : UInt8).toNat` a defeq,
which simplifies proofs.
2024-04-20 16:37:02 +00:00
Sebastian Ullrich
2beb948a3b
feat: System.Platform.target (#3207)
Makes the LLVM triple of the current platform available to Lean code
towards a solution for #2754.

Defaults to the empty string if the compiler is not clang, which can
introduce some divergence between CI and local builds but should not be
noticeable in most cases and is not really possible to avoid.
2024-01-24 12:11:00 +00:00
Leonardo de Moura
ec30da8af7
feat: new implementation for simp (config := { ground := true }) (#3187) 2024-01-18 17:39:06 +00:00
Leonardo de Moura
e11b320cd6 chore: use mathlib naming convention 2024-01-09 12:57:15 +01:00
Leonardo de Moura
2efa9de78a feat: add simprocs for UInt 2024-01-09 12:57:15 +01:00
Leonardo de Moura
b00c13a00e
chore: remove "paper cut" when using Fin USize.size (#2724) 2023-10-24 21:06:35 +11:00
Henrik Böving
24cc6eae6d feat: log2 for Fin and UInts 2022-11-29 01:05:06 +01:00