lean4-htt

History

Scott Morrison d4dca3baac feat: test_extern command (#2970 ) This adds a `test_extern` command. Usage: ``` import Lean.Util.TestExtern test_extern Nat.add 17 37 ``` This: * Checks that the head symbol has an `@[extern]` attribute. * Writes down `t == t'`, where `t` is the term provided, and `t'` is the reference implementation (specifically, `t` with the head symbol unfolded). * Tries to reduce this to `true`, and complains if this fails. Note that the type of the term must have a `BEq` instance for this to work: there's a self-explanatory error message if it isn't available.	2023-12-12 23:33:05 +00:00
..
BadExtern.lean	feat: test_extern command (#2970 )	2023-12-12 23:33:05 +00:00

This adds a `test_extern` command.

Usage:
```
import Lean.Util.TestExtern

test_extern Nat.add 17 37
```

This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.

Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.

2023-12-12 23:33:05 +00:00

BadExtern.lean

feat: test_extern command (#2970 )

2023-12-12 23:33:05 +00:00