rzk-0.8.0: test/typecheck/cases/ill-modal-b-no-dist.rzk
#lang rzk-1 #def b-extract (A : _b U) (x : _b A) : A := x #def ill-b-typed (A B : U) (f : A → <| _b | B |>) : <| _b | A → B |> := mod _b (\ (x : A) → b-extract B (f x))
#lang rzk-1 #def b-extract (A : _b U) (x : _b A) : A := x #def ill-b-typed (A B : U) (f : A → <| _b | B |>) : <| _b | A → B |> := mod _b (\ (x : A) → b-extract B (f x))