Cross Reference: Binder.hascasl
xref: /hets/HasCASL/test/Binder.hascasl
  • Home
  • History
  • Annotate
  • Line#
  • Navigate
  • Download
  • only in ./
Binder.hascasl revision 971cd9553a84c1e1bdbccd0bd63f4fe00b8502f9
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maedervar a, b : Type
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maedertype M : Type -> Type
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederop __ >>= __ : M a * (a ->? M b) ->? M b
971cd9553a84c1e1bdbccd0bd63f4fe00b8502f9Christian Maeder%binder(__ <- __ ;; __)% %binder(do __ <- __ :. __)%
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maedervar p : M a; q : a -> M a
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder
4e013227ed41ccd2e3d09dd44bedd651e1901f38Christian Maeder. def do x <- p :. do y <- q x :. do z <- q y :. q z
971cd9553a84c1e1bdbccd0bd63f4fe00b8502f9Christian Maeder
971cd9553a84c1e1bdbccd0bd63f4fe00b8502f9Christian Maeder. def x <- p ;; y <- q x ;; z <- q y ;; q z

Indexes created Tue Jul 24 14:28:13 CEST 2018