mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
26 lines
972 B
Plaintext
26 lines
972 B
Plaintext
[Compiler.IR] [result]
|
|
def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& tobj) : u8 :=
|
|
case x_1 : tobj of
|
|
MyOption.none →
|
|
let x_2 : u8 := 0;
|
|
ret x_2
|
|
MyOption.some →
|
|
let x_3 : u8 := 1;
|
|
ret x_3
|
|
def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0._boxed (x_1 : tobj) : tagged :=
|
|
let x_2 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_1;
|
|
dec x_1;
|
|
let x_3 : tagged := box x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
|
|
let x_2 : usize := 0;
|
|
let x_3 : tobj := Array.ugetBorrowed ◾ x_1 x_2 ◾;
|
|
let x_4 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_3;
|
|
ret x_4
|
|
def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
|
|
let x_2 : u8 := isSomeWithInstanceNat x_1;
|
|
dec x_1;
|
|
let x_3 : tagged := box x_2;
|
|
ret x_3
|