Всё-всё, уже осознал и исправился. Попутно осознал, что Агда компилируется в Хаскель именно с ленивыми вызовами. В отличие от Идриса, например, который таки дефолтно строгий. Из-за чего If там имеет вполне ожидаемый тип (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2015-03-03 03:04 pm (UTC)Попутно осознал, что Агда компилируется в Хаскель именно с ленивыми вызовами. В отличие от Идриса, например, который таки дефолтно строгий. Из-за чего If там имеет вполне ожидаемый тип
(b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a