mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
34 lines
834 B
Lean4
34 lines
834 B
Lean4
structure A :=
|
||
(a : Nat)
|
||
|
||
structure B :=
|
||
(a : Nat)
|
||
|
||
structure C :=
|
||
(a : Nat)
|
||
|
||
instance : HasCoe A B := ⟨fun s => ⟨s.1⟩⟩
|
||
instance : HasCoe A C := ⟨fun s => ⟨s.1⟩⟩
|
||
|
||
def f {α} (a b : α) := a
|
||
def forceB {α} (b : B) (a : α) := a
|
||
def forceC {α} (c : C) (a : α) := a
|
||
def forceA {α} (a : A) (o : α) := o
|
||
|
||
def f1 (x : _) (y : _) (z : _) :=
|
||
let a1 := f x y;
|
||
let a2 := f y z;
|
||
forceB x a1 -- works
|
||
|
||
def f2 (x : _) (y : _) (z : _) :=
|
||
let a1 := f x (coe y);
|
||
let a2 := f (coe y) z;
|
||
forceB x (forceC z (forceA y (a1, a2))) -- works because we manually added the coercions above
|
||
|
||
def f3 (x : _) (y : _) (z : _) :=
|
||
let a1 := f x y;
|
||
let a2 := f y z;
|
||
/- Fails because we "missed" the opportunity to insert coercions around `y`.
|
||
I think we should **not** support this kind of example. -/
|
||
forceB x (forceC z (forceA y (a1, a2)))
|