mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 18:53:42 +03:00
Look under . for function name on lhs
Need this to rule out some ambiguous names. Fixes #204.
This commit is contained in:
parent
fc0cfcb22b
commit
1dd81ff10b
7
docs/reference/envvars.rst
Normal file
7
docs/reference/envvars.rst
Normal file
@ -0,0 +1,7 @@
|
||||
.. _ref-sect-envvars:
|
||||
|
||||
*********************
|
||||
Environment Variables
|
||||
*********************
|
||||
|
||||
[TODO: Fill in the environment variables recognised by Idris 2]
|
@ -17,3 +17,4 @@ This is a placeholder, to get set up with readthedocs.
|
||||
:maxdepth: 1
|
||||
|
||||
packages
|
||||
envvars
|
||||
|
@ -262,6 +262,7 @@ pruneByType env target alts
|
||||
-- if there's any concrete matches, drop the non-concrete
|
||||
-- matches marked as '%allow_overloads' from the possible set
|
||||
then do keep <- filterCore (notOverloadable defs) matches
|
||||
log 10 $ "Keep " ++ show keep
|
||||
pure (map snd keep)
|
||||
else pure (map snd matches)
|
||||
if isNil res
|
||||
|
@ -562,6 +562,7 @@ getFn (IApp _ f arg) = getFn f
|
||||
getFn (IWithApp _ f arg) = getFn f
|
||||
getFn (IImplicitApp _ f _ _) = getFn f
|
||||
getFn (IAs _ _ _ f) = getFn f
|
||||
getFn (IMustUnify _ _ f) = getFn f
|
||||
getFn f = f
|
||||
|
||||
-- Everything below is TTC instances
|
||||
|
@ -72,7 +72,7 @@ idrisTests
|
||||
-- Records, access and dependent update
|
||||
"record001", "record002",
|
||||
-- Miscellaneous regressions
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005",
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006",
|
||||
-- Totality checking
|
||||
"total001", "total002", "total003", "total004", "total005",
|
||||
"total006",
|
||||
|
20
tests/idris2/reg006/Cmd.idr
Normal file
20
tests/idris2/reg006/Cmd.idr
Normal file
@ -0,0 +1,20 @@
|
||||
data MyCmd : Type -> Type where
|
||||
Display : String -> MyCmd ()
|
||||
Input : MyCmd String
|
||||
|
||||
Pure : ty -> MyCmd ty
|
||||
(>>=) : MyCmd a -> (a -> MyCmd b) -> MyCmd b
|
||||
|
||||
runMyCmd : MyCmd a -> IO a
|
||||
runMyCmd (Display str) = putStrLn str
|
||||
runMyCmd Input = do str <- getLine
|
||||
pure str
|
||||
runMyCmd (Pure x) = pure x
|
||||
runMyCmd (c >>= f) = do res <- runMyCmd c
|
||||
runMyCmd (f res)
|
||||
|
||||
myCmdTest : MyCmd ()
|
||||
myCmdTest = do Display "Hello"
|
||||
x <- Input
|
||||
Display x
|
||||
Pure ()
|
1
tests/idris2/reg006/expected
Normal file
1
tests/idris2/reg006/expected
Normal file
@ -0,0 +1 @@
|
||||
1/1: Building Cmd (Cmd.idr)
|
3
tests/idris2/reg006/run
Executable file
3
tests/idris2/reg006/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --check Cmd.idr
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user