mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 03:34:13 +03:00
Fix regression with making class bodies
:ac should add a class body when given a class name, but a previous change stopped this working. Test added to prevent similar accidents in future.
This commit is contained in:
parent
70b6c862f5
commit
6011227566
@ -541,6 +541,10 @@ Extra-source-files:
|
||||
test/interactive010/expected
|
||||
test/interactive010/input
|
||||
test/interactive010/run
|
||||
test/interactive011/expected
|
||||
test/interactive011/input
|
||||
test/interactive011/run
|
||||
test/interactive011/*.idr
|
||||
|
||||
test/io001/run
|
||||
test/io001/*.idr
|
||||
|
@ -362,7 +362,7 @@ getClause :: Int -- ^ line number that the type is declared on
|
||||
-> Idris String
|
||||
getClause l fn un fp
|
||||
= do i <- getIState
|
||||
case lookupCtxt fn (idris_classes i) of
|
||||
case lookupCtxt un (idris_classes i) of
|
||||
[c] -> return (mkClassBodies i (class_methods c))
|
||||
_ -> do ty_in <- getInternalApp fp l
|
||||
let ty = case ty_in of
|
||||
|
3
test/interactive011/expected
Normal file
3
test/interactive011/expected
Normal file
@ -0,0 +1,3 @@
|
||||
show x = ?Show_rhs_1
|
||||
showPrec d x = ?Show_rhs_2
|
||||
append [] _ = ?append_rhs_1
|
2
test/interactive011/input
Normal file
2
test/interactive011/input
Normal file
@ -0,0 +1,2 @@
|
||||
:ac 5 Show
|
||||
:ac 7 append
|
11
test/interactive011/interactive011.idr
Normal file
11
test/interactive011/interactive011.idr
Normal file
@ -0,0 +1,11 @@
|
||||
import Data.Vect
|
||||
|
||||
data Foo = Bar | Baz
|
||||
|
||||
instance Show Foo where
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
append (x :: xs) ys = ?append_rhs_2
|
||||
|
||||
|
||||
|
3
test/interactive011/run
Executable file
3
test/interactive011/run
Executable file
@ -0,0 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --quiet interactive011.idr < input
|
||||
rm -f *.ibc
|
Loading…
Reference in New Issue
Block a user