6625656940
The semantics was weird. It seems Agda is also having problems with
it. Here is an example that demonstrates how weird the semantics is:
```lean
check (fun {β α} (a : α) (b : β) => (b, a) : {α : Type} → {β : Type} → (a : α) → (b : β) → β × α)
-- Same example using `def`
def f : {α : Type} → {β : Type} → α → β → β × α :=
fun {β : Type} {α : Type} (a : α) (b : β) => (b, a)
```
Both commands were being accepted before this commit. Note that it
flips `β` and `α`.
Here is an example that did not work before this commit and would
confuse users.
```lean
check
let id := fun {α} (a : α) => a;
id [id 1]
```
users would have to write
```lean
check
let id {α} (a : α) := a;
id [id 1]
```
@Kha The Delaborator.lean test broke and I "fixed" by removing the
`{}` from it, and copying `produced` over `expected`. Please make sure
it still makes sense.
28 lines
687 B
Text
28 lines
687 B
Text
import Init.Lean
|
|
|
|
open Lean
|
|
open Lean.Elab
|
|
open Lean.Elab.Term
|
|
|
|
set_option trace.Elab.debug true
|
|
|
|
def tst1 : TermElabM Unit := do
|
|
opt ← getOptions;
|
|
stx ← `(forall (a b : Nat), Nat);
|
|
dbgTrace "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
|
|
e ← elabTermAndSynthesize stx none;
|
|
logDbgTrace (">>> " ++ e); -- display message when `trace.Elab.debug` is true
|
|
dbgTrace "message 2"
|
|
|
|
#eval tst1
|
|
|
|
def tst2 : TermElabM Unit := do
|
|
opt ← getOptions;
|
|
let a := mkTermId `a;
|
|
let b := mkTermId `b;
|
|
stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
|
|
e ← elabTermAndSynthesize stx none;
|
|
logDbgTrace (">>> " ++ e);
|
|
throwErrorIfErrors
|
|
|
|
#eval tst2
|