max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
35801 commits 1 branch 0 tags 5.3 GiB
Commit graph

14 commits

Author SHA1 Message Date
David Thrane Christiansen
1a0d2b6fc1
doc: Char docstring proofreading (#7198) 
This PR makes the docstrings in the `Char` namespace follow the
documentation conventions.

---------

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
 2025-03-08 22:17:01 +00:00
Markus Himmel
b38da34db2
chore: rename BitVec.ofNatLt -> BitVec.ofNatLT (#7064) 
This PR renames `BitVec.ofNatLt` to `BitVec.ofNatLT` and sets up
deprecations for the old name.
 2025-02-13 12:52:31 +00:00
Kim Morrison
222abdd43d
feat: simprocs for other Fin operations (#6295) 
This PR sets up simprocs for all the remaining operations defined in
`Init.Data.Fin.Basic`
 2024-12-03 04:42:17 +00:00
Kim Morrison
6d495586a1
chore: deprecate Fin.ofNat (replaced by Fin.ofNat', subsequently to be renamed) (#6242) 
This PR deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an
`[NeZero]` instance, rather than returning an element of `Fin (n+1)`).

After leaving the deprecation warning in place for some time, we will
then rename `ofNat'` back to `ofNat`.
 2024-11-28 05:23:23 +00:00
Kim Morrison
09e1a05ee9
chore: cleanup imports (#5825) 2024-10-23 23:51:13 +00:00
Kim Morrison
af03af5037
feat: simprocs for #[1,2,3,4,5][2] (#4765) 
None of these were working previously:

```
#check_simp #[1,2,3,4,5][2]  ~> 3
#check_simp #[1,2,3,4,5][2]? ~> some 3
#check_simp #[1,2,3,4,5][7]? ~> none
#check_simp #[][0]? ~> none
#check_simp #[1,2,3,4,5][2]! ~> 3
#check_simp #[1,2,3,4,5][7]! ~> (default : Nat)
#check_simp (#[] : Array Nat)[0]! ~> (default : Nat)
```
 2024-07-17 03:05:17 +00:00
Henrik Böving
18264ae62e
feat: getBitVecValue? understands BitVec.ofNatLt (#4391) 2024-06-07 17:43:08 +00:00
Leonardo de Moura
ff37e5d512
feat: add grind core module (#4249) 2024-05-22 03:50:36 +00:00
Leonardo de Moura
8b2710c8b3 chore: use let_expr to cleanup code 2024-03-02 10:07:15 -08:00
Leonardo de Moura
e53ae5d89e
chore: remove leftovers (#3537) 2024-02-29 02:12:08 +00:00
Leonardo de Moura
855fbed024
fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
Leonardo de Moura
72d233d181
fix: match patterns containing int values and constructors (#3496) 2024-02-25 17:44:08 +00:00
Leonardo de Moura
056cb75ee0 fix: match literal pattern support 
The equation lemmas were not using the standard representation for literals.
 2024-02-24 16:08:07 -08:00
Leonardo de Moura
335fef4396 feat: add helper functions for recognizing builtin literals 2024-02-24 16:08:07 -08:00