leanprover-community / leanprover-community/mathlib4

Write a custom elaborator/unification hint to help with matrix multiplication elaboration

Open
#6,607 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Lean
Stars
4.1k
Forks
1.7k
No merged PRs in 30d

Description

After #6487, Lean has trouble with:

  • A * ↑U where U : (Matrix m m 𝔸)ˣ; it cannot work out what coercion is intended without a full type annotation (or using .val instead)
  • (f.toMatrix * M) i j where f : l ≃. m; it cannot work out the coefficient type of f.toMatrix, and needs the ) to be replaced with :) to elaborate.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the two failing expressions in the issue and investigate the elaboration changes introduced by #6487. Done means both matrix-multiplication forms elaborate without a full type annotation, using .val, or changing ) to :).

Written by the indexing model from the issue text.

Assessment

Domain
compilers
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
25/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.