Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shallow embedding of ArrayPut and ArrayTake #383

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Shallow embedding of ArrayPut and ArrayTake #383

wants to merge 4 commits into from

Commits on Aug 21, 2020

  1. Shallow embedding of ArrayPut and ArrayTake

    Ambroise Lafont authored and Ambroise Lafont committed Aug 21, 2020
    Configuration menu
    Copy the full SHA
    2d076d8 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2020

  1. Vincent's modification to map2 shallow compilation

    @amblafont
    amblafont committed Oct 6, 2020
    Configuration menu
    Copy the full SHA
    8d8cccf View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2020

  1. Shallow compilation of map2 exprs by inlining iso btw record/pairs 

    array_map2 : "('a ⇒ 'b ⇒ 'a × 'b) ⇒ 'a list ⇒ 'b list ⇒ ('a list × 'b list)" is defined in isabelle. But cogent pairs are compiled to some record, thus necessating to insert coercions before and after calling this map2
    @amblafont
    amblafont committed Oct 7, 2020
    Configuration menu
    Copy the full SHA
    d005bc6 View commit details
    Browse the repository at this point in the history

  2. typo

    @amblafont
    amblafont committed Oct 7, 2020
    Configuration menu
    Copy the full SHA
    4bc2eb5 View commit details
    Browse the repository at this point in the history