packages feed

idris-0.12.3: test/regression002/baddoublebang.idr

module baddoublebang

-- Check that two bang bindings running together don't work

doubleBang : Maybe (Maybe Nat) -> Maybe Nat
doubleBang mmn = do pure !!mmn