Kazuhiko Sakaguchi

icon indicating an email [email protected]

icon location Lyon, France icon location Postdoc in the Plume team at CNRS, ENS de Lyon, UCBL, LIP | Interests: interactive theorem proving, formalization of mathematics, and proof by reflection

Results 307 comments of Kazuhiko Sakaguchi

Fix the scope of arguments of intmul

I'm unavailable this week (Dagstuhl) but I advocate using number notations only for `nat` and `int` literals.

Fix the scope of arguments of intmul

I just noticed that Nov. 1st is a public holiday in France.

Spurious warning `Projection value has no head constant`

We usually write `-arg -w -arg -projection-no-head-constant` in `_CoqProject` to suppress this warning.

`#[primitive] HB.mixin` breaks the types of constants lifting mixin projections

@gares Can you point out the part of the code declaring these constants and synthesizing their types? I have a rough idea of how to fix the issue.

`#[primitive] HB.mixin` breaks the types of constants lifting mixin projections

Thanks. I believe that constructing the types of these constants from the declaration of the record type is much easier than doing so from the types of the projections. While...

`#[primitive] HB.mixin` breaks the types of constants lifting mixin projections

I will take a closer look when I have some time.

Clean up extra_*.v material

FTR, `floorQ` in `floor.v` should now be replaced by `Num.floor` (defined in `archimedean.v` for any `archiNumDomainType`).

Clean up extra_*.v material

> FTR, `floorQ` in `floor.v` should now be replaced by `Num.floor` (defined in `archimedean.v` for any `archiNumDomainType`). Done in #24.

Add tests for reverse dependencies to CI

Since Apery is now compatible with MC2, we should be able to test Apery in CI. But I don't know how to do that.

Revert #90

Thanks. I'm unsure if I want to revert it now, but I will open a PR to do so.