Sitelet https://github.com/math-comp/math-comp/pull/1602
Skip to content

Use binary parser for rat Number Notation - #1602

Draft
hoheinzollern wants to merge 1 commit into
math-comp:masterfrom
hoheinzollern:rat-fast-parser
Draft

hoheinzollern wants to merge 1 commit into
math-comp:masterfrom
hoheinzollern:rat-fast-parser

Conversation

@hoheinzollern

Copy link
Copy Markdown
Member
Motivation for this change

Fixes slow parsing of large rational numbers. Vibe-coded, needs proper review and discussion.

Minimal TODO list
  • added changelog entries with doc/changelog/make-entry.sh
  • added corresponding documentation in the headers
  • tried to abide by the contribution guide
  • this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

Comment thread algebra/rat.v
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From Corelib Require Import PosDef.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We may not want to go to binary N or Z, keeping the value behind a locked Decimal -> rat should be enough.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants