Joe Hendrix 75272cb157 feat: BitVec.ofNatLt and updates to use it (#3430) ... This PR is an effort to improve reasoning at the Nat level about bitvectors and reduce of Fin and Nat. It slightly tightens some proofs, but is generally aimed at reducing inconsistencies between definitions at the Nat and Fin types in favor of more consistently using Nat operations. This ports leanprover/std4#664 to Lean core. Here was the rational I provided in the discussion for leanprover/std4#664: It's mostly about consistency. If we use the same types and style in definitions and proofs, there is less surprise when unfolding or otherwise using definitions. We use some Nat based operations that haven't been extended to Fin such as the bitwise operations, and I don't want to pay the overhead of introducing a Fin version of every Bitvector operation. So this basically means Nat is preferred. One argument potentially in favor of Fin is that we could reuse results proven there, but that doesn't really seem to be the case so far. A second argument is that we want to simplify expression to use more canonical forms and we currently can pretty-print those operations better using ofNat than ofFin. We could define the notations using ofFin of course though, but that's additional operators that will show up in expressions.		2024-02-21 18:02:56 +00:00
..
533.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
533.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
863.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
863.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
1031.lean
1031.lean.expected.out
1265.lean
1265.lean.expected.out	chore: upstream solve_by_elim (#3408)	2024-02-21 01:16:04 +00:00
1403.lean
1403.lean.expected.out	feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences (#2539)	2024-01-03 00:01:40 +00:00
1525.lean	fix: missing info tree on elab failure	2023-01-26 13:05:57 +01:00
1525.lean.expected.out	fix: missing info tree on elab failure	2023-01-26 13:05:57 +01:00
1659.lean	feat: auto-complete declaration names in arbitrary namespaces	2023-07-28 07:50:09 -07:00
1659.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
amb.lean
amb.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
anonHyp.lean
anonHyp.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
autoBoundIssue.lean
autoBoundIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
catHover.lean
catHover.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
codeaction.lean	fix: version numbers in code actions (#2721)	2023-10-24 22:55:47 +11:00
codeaction.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
compHeader.lean
compHeader.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion.lean
completion.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion2.lean
completion2.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion3.lean
completion3.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion4.lean
completion4.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion5.lean
completion5.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion6.lean
completion6.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completion7.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
completion7.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionAtPrint.lean
completionAtPrint.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionDocString.lean
completionDocString.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionEOF.lean
completionEOF.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionIStr.lean
completionIStr.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionOption.lean
completionOption.lean.expected.out	feat: upstream 'Try this:' widgets (#3266)	2024-02-13 21:58:36 +00:00
completionPrefixIssue.lean
completionPrefixIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
completionPrv.lean
completionPrv.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
compNamespace.lean
compNamespace.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
definition.lean
definition.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
Diff.lean
Diff.lean.expected.out
discrsIssue.lean
discrsIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
dotIdCompletion.lean
dotIdCompletion.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
editAfterError.lean
editAfterError.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
editCompletion.lean
editCompletion.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
fieldCompletion.lean
fieldCompletion.lean.expected.out	chore: set literal notation (#3348)	2024-02-19 23:22:36 +00:00
foldingRange.lean
foldingRange.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goalEOF.lean
goalEOF.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goalIssue.lean
goalIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goTo.lean	feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767)	2023-01-19 09:10:01 +00:00
goTo.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
goTo2.lean	feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767)	2023-01-19 09:10:01 +00:00
goTo2.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
haveInfo.lean
haveInfo.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
highlight.lean
highlight.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hover.lean	feat: improve termination_by error messages (#3255)	2024-02-05 13:13:53 +00:00
hover.lean.expected.out	doc: fix typos (#3236)	2024-02-01 19:03:58 +00:00
hoverAt.lean
hoverAt.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverBinderUndescore.lean
hoverBinderUndescore.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverDot.lean
hoverDot.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
hoverException.lean
hoverException.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
infoIssues.lean
infoIssues.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
internalNamesIssue.lean
internalNamesIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
inWordCompletion.lean	feat: BitVec.ofNatLt and updates to use it (#3430)	2024-02-21 18:02:56 +00:00
inWordCompletion.lean.expected.out	feat: BitVec.ofNatLt and updates to use it (#3430)	2024-02-21 18:02:56 +00:00
jumpMutual.lean
jumpMutual.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
keywordCompletion.lean	test: make completion tests less dependent on core	2023-07-28 07:50:09 -07:00
keywordCompletion.lean.expected.out	chore: upstream Std.Util.ExtendedBinders (#3320)	2024-02-14 11:36:00 +00:00
lean3HoverIssue.lean
lean3HoverIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
macroGoalIssue.lean
macroGoalIssue.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
match.lean
match.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
matchPatternHover.lean
matchPatternHover.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
matchStxCompletion.lean
matchStxCompletion.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
partialNamespace.lean
partialNamespace.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
plainGoal.lean	fix: report goals in induction with parse error	2023-11-20 09:15:27 +01:00
plainGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
plainTermGoal.lean
plainTermGoal.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
rename.lean	feat: rename request handler (#2462)	2023-11-21 13:10:52 +01:00
rename.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
run.lean	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00
stdOutput.lean
stdOutput.lean.expected.out
test_single.sh
unterminatedDocComment.lean
unterminatedDocComment.lean.expected.out	feat: per-package server options (#2858)	2023-11-26 13:42:38 +00:00
userWidget.lean	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00
userWidget.lean.expected.out	feat: bundle of widget improvements (#2964)	2023-12-21 06:24:33 +00:00