mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
d9ebd51c04
This PR adds support for ignoring user defined borrow annotations. This can be useful when defining `extern`/`export` pairs as the `extern` might be infected by borrow annotations while in `export` they are already ignored.
39 lines
799 B
Lean4
39 lines
799 B
Lean4
module
|
||
|
||
/-!
|
||
This test asserts that disabling user-defined borrow annotations works. This is sometimes required for
|
||
export/extern pairs
|
||
-/
|
||
|
||
public abbrev Foo (α : Type) := (x : @& α) → α
|
||
|
||
/--
|
||
trace: [Compiler.result] size: 0
|
||
def t1 @&x : tobj :=
|
||
extern
|
||
[Compiler.result] size: 2
|
||
def t1._boxed x : tobj :=
|
||
let res := t1 x;
|
||
dec x;
|
||
return res
|
||
-/
|
||
#guard_msgs in
|
||
set_option trace.Compiler.result true in
|
||
@[extern "t1"]
|
||
public opaque t1 : Foo Nat
|
||
|
||
/--
|
||
trace: [Compiler.result] size: 0
|
||
def t2 x : tobj :=
|
||
extern
|
||
[Compiler.result] size: 1
|
||
def t2._boxed x : tobj :=
|
||
let res := t2 x;
|
||
return res
|
||
-/
|
||
#guard_msgs in
|
||
set_option compiler.ignoreBorrowAnnotation true in
|
||
set_option trace.Compiler.result true in
|
||
@[extern "t2"]
|
||
public opaque t2 : Foo Nat
|