3 ms·
Agda has proof search, yes. But for example if you write down the expression for `and` with type holes: and : Bool -> Bool -> Bool and a false = { }0 and
by freyrs3 13y ago
Agda has proof search, yes. But for example if you write down the expression for `and` with type holes:
and : Bool -> Bool -> Bool
and a false = { }0
and a true = { }1
It will deduce the following which is well-typed but not correct.
and : Bool -> Bool -> Bool
and true false = false
and false true = false
If the types are precise and highly constrained it works well, but it's imperfect.
- dllthomas 13y agoI think you left out the wrong case (and another right one). Also, while this is the same functionality, it shouldn't really be expected to work well when dealing with concrete types - you're not nearly as constrained as when you have a bunch of polymorphic terms in the relevant type signatures - like was the case in the article here.