Comments (2)
edwinb
commented on May 16, 2024
I'm not sure, to be honest, I haven't really thought about it too deeply. Something like Agda's approac would be good (http://www2.tcs.ifi.lmu.de/~abel/foetus.pdf) but I don't know too much about it. It probably needs a complete rewrite to be honest.
from idris-dev.
edwinb
commented on May 16, 2024
I'll close this, since the totality checker now does mutually recursive functions by checking how the size of each argument changes across the call graph - however, there's lots of ways it could still be improved if you still want to hack on it.
from idris-dev.
Related Issues (20)
- Types appear to match but fail HOT 4
- Totality checker thinks simple function is total when it's not HOT 1
- Broken sections of custom operators starting with pipe '|', "expecting function name"
- in interfaces.rst, replace "brackets" by "parentheses" HOT 3
- Totality check fails on simple structural recursion when it is not tail recusive
- Dependent constructor reproted as not strictly positive when in mutual block HOT 1
- Installation from hackage fails with ghc 8.10.2 in cabal configuration step HOT 1
- Is there a color scheme for IntelliJ?
- Idris not located in terminal.
- Please update dependency upperbounds HOT 2
- `pkg010` test output depends on version of optparse-applicative library used
- Lambda in place of Type HOT 1
- Data.Primitives.Views.divides behaves odd with negative dividend
- idris-1.3.3 fails with haskeline-0.8 HOT 2
- Type checker confused by overloaded `fst` (or just a strange error message)
- Test ffi008 fails with "multiple definition of `mystruct'"
- Cannot define recursive bound on associated type of an interface
- Incorrect behaviour when resolving associated type of an interface
- List available operators
- Dead download link for idris-1.3.3-win64.exe HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris-dev.