mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
26 lines
763 B
Lean4
26 lines
763 B
Lean4
def forceNat (a : Nat) := true
|
|
def forceInt (a : Int) := false
|
|
|
|
def f1 :=
|
|
/-
|
|
The following example works, but it adds a coercion at `forceInt i`.
|
|
The elaborated term is
|
|
```
|
|
fun (n i : Nat) => if n == i then forceNat n else forceInt (coe i)
|
|
```
|
|
-/
|
|
fun n i => if n == i then forceNat n else forceInt i -- works
|
|
|
|
def f2 :=
|
|
fun n i => if coe n == i then forceInt i else forceNat n -- works
|
|
|
|
#check f1 -- Nat → Nat → Bool
|
|
#check f2 -- Nat → Int → Bool
|
|
|
|
def f3 :=
|
|
/- Fails.
|
|
- `n == i` generates type constraint enforcing `n` and `i` to have the same type.
|
|
- `forceInt i` forces `i` (and consequently `n`) to have type `Int`.
|
|
- `forceNat n` fails because there is no coercion from `Nat` to `Int`. -/
|
|
fun n i => if n == i then forceInt i else forceNat n
|