21 (* \infer{c1 c2 ~> c1' c2}{c1 ~> c1'} *) 22 | whnf g (c as Capp (c1, c2)) = if (squig c1) then whnf g (Capp (whnf g c1, c2)) else c 23 (* \infer{pi c ~> pi c'}{c ~> c'} *) 24 | whnf g (c as Cpi1 c') = if (squig c') then whnf g (Cpi1 (whnf g c')) else c 25 | whnf g (c as Cpi2 c') = if (squig c') then whnf g (Cpi2 (whnf g c')) else c 26 (* the infamous \not\rightsquigarrow as per http://cmubash.org/?1991 27 * now actually we need to invoke natural kind *) 28 | whnf g c = 29 (case naturalKind g c of 30 Ksing c' => whnf g c' 31 | _ => c)