rzk-0.9.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))