Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Merge Requests
  • !23

Merged
Opened Nov 17, 2016 by Jacques-Henri Jourdan@jjourdanMaintainer

Fractional typeclass.

  • Overview 34
  • Commits 1
  • Changes 5

A typeclass for fractional assertions, that is assertions that depend on a fraction and that can be split.

This is used to derive generically a few other instances for framing , destructing, combining and spliting assertions of sums of fractions. I found it usefull when doing fraction-heavy proofs in LambdaRust.

The Right Way To Do It would be to use a typeclass over the predicate itself. Unfortunately, the unification algorithm of typeclasses is not powerful enough to do the right beta-expansion that would expose the predicate applied to some fraction. Instead, the Fractional type class has as parameters both the predicate and the applied form that can be directly unified with the fractured assertion. Not very pretty.

I wonder whether I should split this into two type classes: the first one would depend only on the predicate and would actually state the fractionality of it, and the second would do the beta-expansion job. What do you think?

Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!23
Source branch: jh/fractional