git.iko.soy/Idris-dev
on 7afa310 help sign in
history oftest/reg018/expected
all commits
a1fb7a3Inline with blocksEdwin Brady a6caf2dShow more errorsDavid Raymond Christiansen b0720b0Change guardedness check for new-style coinductionEdwin Brady 57c8657Added column name to sourceAhmad Salim Al-Sibahi 99a8a66Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.Edwin Brady 56bd9a1Look through call graph for mutual recursion when productivity checking Otherwise we might miss non-productive calls, particularly important when using 'with'. Fixes issue #183Edwin Brady