| axiom TrustMe {p : Prop} : p | |
| def x := (1, 2) | |
| def y := x | |
| @[noinline] def mk (v : Nat) := (v, v+1) | |
| #eval withPtrAddr x (fun a => dbgTrace (">> " ++ toString a) $ fun _ => 0) TrustMe | |
| /-- info: true -/ | |
| #guard_msgs in | |
| #eval withPtrEq x y (fun _ => dbgTrace (">> " ++ toString x ++ " == " ++ toString y) $ fun _ => x == y) TrustMe -- should not print message | |
| /-- | |
| info: >> (1, 2) == (1, 2) | |
| --- | |
| info: true | |
| -/ | |
| #guard_msgs in | |
| #eval withPtrEq x (mk 1) (fun _ => dbgTrace (">> " ++ toString x ++ " == " ++ toString y) $ fun _ => x == y) TrustMe -- should print message |