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
module baddoublebang -- Check that two bang bindings running together don't work doubleBang : Maybe (Maybe Nat) -> Maybe Nat doubleBang mmn = do pure !!mmn