commit: 9519f8445ee80845948bab85c53dbb3b6238d628

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Fri Sep 04 15:15:50 2026 +0000
committer: Sebastian Ullrich <sebasti@nullri.ch>

Fri Sep 04 15:15:59 2026 +0000
tree: c836156b8d645a7104500ef2dbfd421c56864a2c
parent: 53ccd6d212f05a036de6ffe298bedee038c933da [diff]

test: drop the comment restating `trim`'s loop condition in the `mpn` model

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

tests/elab/mpn_model.lean[diff]

1 file changed

tree: c836156b8d645a7104500ef2dbfd421c56864a2c

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.