-
Notifications
You must be signed in to change notification settings - Fork 0
/
ide_features.txt
32 lines (30 loc) · 1.94 KB
/
ide_features.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Features that are good to have in IDE support for Dhall:
- Display typechecking and syntax errors
- Collapse/expand code regions: "let" definitions, lists, records, if/then/else
- Go to definition of any variable, go to usages for any variable
- Load imported files and navigate in them, keeping them read-only
- Tooltip: hover on a variable to see its type, or display its type on Command-hover or otherwise
- Type error: say where and what types were expected and what types were found instead
- Autocomplete possible arguments for curried functions
- Autocomplete possible functions that apply to a given argument type
- Autocomplete constructor names after union types and record field names after record types / names
- Autocomplete lambdas in `merge`
- Autocomplete defined variables in scope
- Autocomplete lambda blocks after type annotation is given
- Do not autocomplete the name that is currently being defined (no recursion in Dhall!)
- Fill in the inferred type for let bindings or lambda arguments or any other terms
- Reduce to normal form and replace selected expression
- Alpha-normalize, beta-normalize, eta-reduce inline
- Freeze / unfreeze imports
- Rename variables within their definition's scope
- Suggest edits when typechecking fails or when variables are undefined
- When assert fails, show the two unequal asserted values in normal form
- Autocomplete available symbols that can be imported from known already imported files or from the standard prelude
- Autocomplete available functions that may be left-applied to a given value
- Autoformat the Dhall code, even if it does not typecheck
- Infer type for an expression and create a separate type value
- Refactor a value from a subexpression into a local variable
- Inline a local variable into places where it is used, eliminating the local variable
- Use `curryhoward` to generate code when possible; or "derive functor", etc.
- Work with typed holes
- Simplify arithmetic with Bool, Natural, Integer