2120883307
@Kha I had some unexpected surprises, but it is a good change.
Here is the summary.
1- We could get rid of `a %ₙ b` and `ModN` class. We can use `HMod`
instead. It was a positive surprise since I didn't remember we had
this `ModN` class.
2- Coercions are never used in heterogeneous operators. This is
expected since `a * b` is now notation for `HMul.hMul a b`, and
`a` and `b` may have different types. I manually added instances such
as `HMul Nat Int Int`. However, I did not try to add generic instances
such as
```
instance [Coe a b] [Mul b] : HMul a b b where
hMul x y := mul (coe x) y
```
I will try later.
3- Give `h : cs.size > 0`, I got a type error at
```
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩
```
`Nat.predLt h` has type `Nat.pred cs.size < cs.size`
However, `Nat.pred cs.size` doesn't unify with `cs.size - 1`.
The problem is that we can't synthesize the `HSub` instance until
we apply the default instances.
It worked before because `isDefEq` would force the pending TC
problem `Sub Nat` to be resolved, and after that we would be able
to reduce `cs.size - 1` and establish that it is definitionally
equal to `Nat.pred cs.size`.
I considered two possible workarounds
a) `let idx : Fin cs.size := ⟨cs.size - (1:Nat), Nat.predLt h⟩`
b) `let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.predLt h⟩`
The first one works because we are not providing enough information
for synthesizing the `HSub` instance. The second works because it
postpones the elaboration of `Nat.predLt h`. The default instances
will be applied before we start applying tactics.
4- The `.` notation is affected too. For example, `(x + 1).toUInt8`
doesn't work since we don't know the type of `x+1` until we apply
default instances. I fixed it by using `(x + (1:Nat)).toUInt8`.
Another possible fix is `Nat.toUInt8 (x + 1)`.
Similarly, `(x+1).fold ...` doesn't work.
5- The following code failed to be elaborated
```
indent (push s!"{ss'}\n") (some (0 - Format.getIndent (← getOptions)))
```
It was working before, but it relied on how the expected type is
propagated. The elaborator process
```
some (0 - Format.getIndent (← getOptions))
```
with expected type `(Option Int)`. So, the `-` is interpreted as
`Int.sub` although `Format.getIndent (← getOptions)` has type `Nat`.
In the new `HSub`, the expected type doesn't really influence TC
resolution since it is an `outparam`. So, we failed with the error
failed to synthesize `HSub Nat Nat Int`.
One possible fix was to add the instance `HSub Nat Nat Int` with
`Int.sub`, but I used the following fix
```
some ((0 : Int) - Format.getIndent (← getOptions))
```
which makes it clear that we want the `Int.sub` operator instead of
`Nat.sub`.
52 lines
1.3 KiB
Text
52 lines
1.3 KiB
Text
example : Prop := ∀ n, (n:Nat) + n = n.succ
|
||
example : Prop := ∀ n, n.succ = (n:Nat) + n
|
||
example : Prop := ∀ n, (n:Nat) + n.succ = n
|
||
example : Prop := ∀ n, n.succ + (n:Nat) = n
|
||
example : Prop := ∀ n, (n.succ:Nat) + n = n
|
||
example : Prop := ∀ n, (n:Nat).succ + n = n
|
||
|
||
def fib: Nat → Nat
|
||
| 0 => 0
|
||
| 1 => 1
|
||
| n + 2 => fib n + fib (n + 1)
|
||
|
||
theorem fib50Eq : fib 50 = 12586269025 :=
|
||
rfl
|
||
|
||
inductive type : Type
|
||
| A : type
|
||
| B : type
|
||
|
||
inductive val : type → Type
|
||
| cA : val type.A
|
||
| cB : val type.B
|
||
|
||
inductive wrap : Type
|
||
| val : ∀ {t : type}, (val t) → wrap
|
||
|
||
def f : wrap → Nat
|
||
| wrap.val val.cA => 1
|
||
| _ => 1
|
||
|
||
example (a : Nat) : True := by
|
||
have ∀ n, n ≥ 0 → a ≤ a from fun _ _ => Nat.leRefl ..
|
||
exact True.intro
|
||
|
||
example (ᾰ : Nat) : True := by
|
||
have ∀ n, n ≥ 0 → ᾰ ≤ ᾰ from fun _ _ => Nat.leRefl ..
|
||
exact True.intro
|
||
|
||
inductive Vec.{u} (α : Type u) : Nat → Type u
|
||
| nil : Vec α 0
|
||
| cons : α → {n : Nat} → Vec α n → Vec α (Nat.succ n) -- TODO: investigate why +1 doesn't work here
|
||
|
||
constant Vars : Type
|
||
|
||
structure Lang :=
|
||
(funcs : Nat → Type)
|
||
(consts : Type)
|
||
|
||
inductive Term (L : Lang) : Type
|
||
| const_term : L.consts → Term L
|
||
| var_term : Vars → Term L
|
||
| func_term (n : Nat) (f : L.funcs n) (v : Vec (Term L) n) : Term L
|