lean4 feat: generalize simp normal form testing code and validate `Nat`/`Int` normal forms

feat: generalize simp normal form testing code and validate `Nat`/`Int` normal forms

Open joehendrix opened this issue 11 months ago • 1 comments

This is still a work in progress.

Mar 02 '24 00:03 joehendrix

Mathlib CI status (docs):

❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-04-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-04-08 17:59:23)
❌ Mathlib branch lean-pr-testing-3562 built against this PR, but linting failed. (2024-04-12 10:24:20) View Log
❌ Mathlib branch lean-pr-testing-3562 built against this PR, but linting failed. (2024-04-12 10:59:00) View Log

Apr 08 '24 17:04 leanprover-community-mathlib4-bot