9d304df757
@Kha This one required a bunch of manual fixes. The main issue is that
before we added the string interpolation feature, we created
`MessageData`s using `++` and coercions. For example, given
`(e : Expr)`, we would write
```
let msg : MessageData := "type: " ++ e
```
and rely on the coercions `String -> MessageData` and
`Expr -> MessageData`, and the instance `Append MessageData`.
However, heterogeneous operators "block" the expected type propagation downwards.
This kind of code is obsolete now since we can write a more compact
version using string interpolation
```
let msg := m!"type: {e}"
```
20 lines
425 B
Text
20 lines
425 B
Text
syntax:65 [myAdd1] term "+++" term:65 : term
|
|
syntax:65 [myAdd2] term "+++" term:65 : term
|
|
|
|
macro_rules [myAdd1]
|
|
| `($a +++ $b) => `(Nat.add $a $b)
|
|
|
|
macro_rules [myAdd2]
|
|
| `($a +++ $b) => `(Append.append $a $b)
|
|
|
|
#check (1:Nat) +++ 3
|
|
|
|
theorem tst1 : ((1:Nat) +++ 3) = 1 + 3 :=
|
|
rfl
|
|
|
|
#check fun (x : Nat) => if x +++ 3 = x then x else x + 1
|
|
|
|
#check [1, 2] +++ [3, 4]
|
|
|
|
theorem tst2 : ([1, 2] +++ [3, 4]) = [1, 2] ++ [3, 4] :=
|
|
rfl
|