diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean index e1535bef79..a3f2e5c82f 100644 --- a/src/Init/Lean/Elab/BuiltinNotation.lean +++ b/src/Init/Lean/Elab/BuiltinNotation.lean @@ -27,6 +27,9 @@ fun stx expectedType? => do def elabInfixOp (op : Name) : TermElab := fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType? +@[builtinTermElab prod] def elabProd : TermElab := elabInfixOp `Prod +@[builtinTermElab fcomp] def ElabFComp : TermElab := elabInfixOp `Function.comp + @[builtinTermElab add] def elabAdd : TermElab := elabInfixOp `HasAdd.add @[builtinTermElab sub] def elabSub : TermElab := elabInfixOp `HasSub.sub @[builtinTermElab mul] def elabMul : TermElab := elabInfixOp `HasMul.mul @@ -57,7 +60,7 @@ fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType @[builtinTermElab cons] def elabCons : TermElab := elabInfixOp `List.cons @[builtinTermElab andthen] def elabAndThen : TermElab := elabInfixOp `HasAndthen.andthen --- @[builtinTermElab bind] def elabBind : TermElab := elabInfixOp `HasBind.bind +@[builtinTermElab bindOp] def elabBind : TermElab := elabInfixOp `HasBind.bind @[builtinTermElab seq] def elabseq : TermElab := elabInfixOp `HasSeq.seq @[builtinTermElab seqLeft] def elabseqLeft : TermElab := elabInfixOp `HasSeqLeft.seqLeft @@ -73,6 +76,7 @@ fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType @[builtinTermElab andM] def elabAndM : TermElab := elabInfixOp `andM /- +TODO @[builtinTermElab] def elabsubst : TermElab := elabInfixOp infixR " ▸ " 75 -/ diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index ad88d55ae0..67da75e979 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -19,10 +19,14 @@ def two := 2 -- set_option trace.Elab.app true -- set_option trace.Elab true +def act1 : IO String := +pure "hello" + #eval run "#check [zero, one, two]" #eval run "#check id $ Nat.succ one" #eval run "#check HasAdd.add one two" #eval run "#check one + two > one ∧ True" +-- #eval run "#check act1 >>= IO.println" #eval run "universe u universe v