tests/elab/121.lean - third_party/github.com/leanprover/lean4 - Git at Google



            abbrev DelabM := Id

            
            abbrev Delab := DelabM Nat


            example : DelabM Nat := pure 1  -- works

            
            example : Delab := pure 1       -- works


	abbrev DelabM := Id
	abbrev Delab := DelabM Nat

	example : DelabM Nat := pure 1 -- works
	example : Delab := pure 1 -- works