chore: add test
This commit is contained in:
parent
ca28b0462c
commit
d67546e388
2 changed files with 10 additions and 0 deletions
9
tests/lean/instance1.lean
Normal file
9
tests/lean/instance1.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
def Mine := Id
|
||||
|
||||
class MyMonad (m) extends Monad m where
|
||||
bind_eq_bind : @bind = @bind := by trivial
|
||||
|
||||
instance : MyMonad Mine where
|
||||
-- should show me all the fields I need to fill in
|
||||
-- excluding default and auto-param fields
|
||||
-- i.e., only `pure` and `bind`
|
||||
1
tests/lean/instance1.lean.expected.out
Normal file
1
tests/lean/instance1.lean.expected.out
Normal file
|
|
@ -0,0 +1 @@
|
|||
instance1.lean:6:24-6:29: error: fields missing: 'pure', 'bind'
|
||||
Loading…
Add table
Reference in a new issue