HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-08-17 04:50:22 +03:00
Code Issues Packages Projects Releases Wiki Activity
cc0bffb22c
Kind/bootstrap.hvm1
Victor Taelin cc0bffb22c recursive Kind2 file loader works now... 
someone acquired debt today
2024-02-22 23:43:20 -03:00

1723 lines
109 KiB
Plaintext
Raw Blame History

(U60.match 0 z s) = z
(U60.match n z s) = (s (- n 1))
(Str String.nil) = λP λcons λnil nil
(Str (String.cons x xs)) = λP λcons λnil (cons x (Str xs))
(Str.view str) = (str 0 λhλt(String.cons h (Str.view t)) String.nil)
(Strs.view strs) = (List.view λx(Str.view x) strs)
(List.view elem list) = (list 0 λhλt(List.cons (elem h) (List.view elem t)) List.nil)
Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0))))
Book.A = 0
Book.A.bad = λ_P λ_new ((_new 1) 0)
Book.A.sel = λ_P λ_k (U60.match _k (_P (Book.A.one)) λ_tag_1(0))
Book.A.one = λ_P λ_new (_new 0)
Book.BBT.balance.lft_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt
let _P = λ_x (((Book.BBT) _K) _V)
let _bin = λ_lft.size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt
let _P = λ_x 0
let _true = λ_new_size λ_key λ_val λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_rgt
let _lft = ((((((((Book.BBT.lft_rotate) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt)
((((((((Book.BBT.rgt_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
let _false = λ_new_size λ_key λ_val λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_rgt
let _lft = ((((((((Book.BBT.bin) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt)
((((((((Book.BBT.rgt_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
(((((((((((((Book.Cmp.is_gtn) ((_cmp _set_key) _lft.key)) _P) _true) _false) _new_size) _node_key) _val) _lft.key) _lft.val) _lft.lft) _lft.rgt) _rgt)
let _tip = (((Book.BBT.tip) _K) _V)
(((_lft _P) _bin) _tip)
Book.BBT.balance = λ_K λ_V λ_cmp λ_set_key λ_node_key λ_val λ_lft λ_rgt
let _P = λ_x (((Book.BBT) _K) _V)
let _new = λ_lft.size λ_lft
let _P = λ_x (((Book.BBT) _K) _V)
let _new = λ_rgt.size λ_rgt
let _new_size = (+ 1 (((Book.U60.max) _lft.size) _rgt.size))
let _balance = (((Book.U60.abs_diff) _lft.size) _rgt.size)
let _P = λ_x 0
let _true = λ_new_size λ_node_key λ_val λ_lft λ_rgt
let _P = λ_x 0
let _true = (Book.BBT.balance.lft_heavier)
let _false = (Book.BBT.balance_rgt_heavier)
((((((((((((((Book.U60.to_bool) (< _rgt.size _lft.size)) _P) _true) _false) _K) _V) _cmp) _new_size) _node_key) _set_key) _val) _lft) _rgt)
let _false = λ_new_size λ_node_key λ_val λ_lft λ_rgt ((((((((Book.BBT.bin) _K) _V) _new_size) _node_key) _val) _lft) _rgt)
((((((((((Book.U60.to_bool) (> _balance 1)) _P) _true) _false) _new_size) _node_key) _val) _lft) _rgt)
((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new)
((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
Book.BBT.balance_rgt_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt
let _P = λ_x (((Book.BBT) _K) _V)
let _bin = λ_rgt.size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt
let _P = λ_x 0
let _true = λ_new_size λ_key λ_val λ_lft λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt
let _rgt = ((((((((Book.BBT.bin) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt)
((((((((Book.BBT.lft_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
let _false = λ_new_size λ_key λ_val λ_lft λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt
let _rgt = ((((((((Book.BBT.rgt_rotate) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt)
((((((((Book.BBT.lft_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt)
(((((((((((((Book.Cmp.is_gtn) ((_cmp _set_key) _rgt.key)) _P) _true) _false) _new_size) _node_key) _val) _lft) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt)
let _tip = (((Book.BBT.tip) _K) _V)
(((_rgt _P) _bin) _tip)
Book.BBT.bin = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt λ_P λ_bin λ_tip (((((_bin _size) _key) _val) _lft) _rgt)
Book.BBT.from_list = λ_K λ_V λ_cmp λ_list
let _P = λ_x (((Book.BBT) _K) _V)
let _cons = λ_head λ_tail
let _P = λ_x (((Book.BBT) _K) _V)
let _new = λ_key λ_val (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) (((((Book.BBT.from_list) _K) _V) _cmp) _tail))
((_head _P) _new)
let _nil = (((Book.BBT.tip) _K) _V)
(((_list _P) _cons) _nil)
Book.BBT.get = λ_K λ_V λ_cmp λ_key λ_map
let _P = λ_x ((Book.Maybe) _V)
let _bin = λ__size λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _P = λ_x 0
let _ltn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.lft)
let _eql = λ_cmp λ_key (((Book.Maybe.some) _V) _next.val)
let _gtn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.rgt)
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
let _tip = ((Book.Maybe.none) _V)
(((_map _P) _bin) _tip)
Book.BBT.got = λ_K λ_V λ_cmp λ_key λ_map
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _P = λ_x 0
let _ltn = λ_cmp λ_key
let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.lft)
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
let _new = λ_val λ_lft
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _lft) _next.rgt)
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map)
((_new_pair _P) _new)
let _eql = λ_cmp λ_key
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt)
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) (((Book.Maybe.some) _V) _next.val)) _map)
let _gtn = λ_cmp λ_key
let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.rgt)
let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V))
let _new = λ_val λ_rgt
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _rgt)
(((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map)
((_new_pair _P) _new)
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
let _tip = (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) ((Book.Maybe.none) _V)) (((Book.BBT.tip) _K) _V))
(((_map _P) _bin) _tip)
Book.BBT.got_size = λ_K λ_V λ_map
let _P = λ_x (((Book.Pair) 0) (((Book.BBT) _K) _V))
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt)
(((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) _size) _map)
let _tip = (((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) 0) (((Book.BBT.tip) _K) _V))
(((_map _P) _bin) _tip)
Book.BBT.has = λ_K λ_V λ_cmp λ_key λ_map
let _P = λ_x (Book.Bool)
let _bin = λ_next.size λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _P = λ_x 0
let _ltn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.lft)
let _eql = λ_cmp λ_key (Book.Bool.true)
let _gtn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.rgt)
((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key)
let _tip = (Book.Bool.false)
(((_map _P) _bin) _tip)
Book.BBT.has.linear = λ_K λ_V λ_cmp λ_key λ_map
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
let _bin = λ_size λ_node_key λ_val λ_lft λ_rgt
let _P = λ_x 0
let _ltn = λ_cmp λ_size λ_has_key λ_val λ_lft λ_rgt λ_has_key
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
let _new = λ_bool λ_lft
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt)
(((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _map)
((((((((Book.BBT.has.linear) _K) _V) _cmp) _has_key) _lft) _P) _new)
let _eql = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.true)) ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt))
let _gtn = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key
let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V))
let _new = λ_bool λ_rgt
let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt)
(((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _rgt)
((((((((Book.BBT.has.linear) _K) _V) _cmp) _has_key) _rgt) _P) _new)
(((((((((((((_cmp _key) _node_key) _P) _ltn) _eql) _gtn) _cmp) _size) _node_key) _val) _lft) _rgt) _key)
let _tip = (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.false)) (((Book.BBT.tip) _K) _V))
(((_map _P) _bin) _tip)
Book.BBT = λ_K λ_V 0
Book.BBT.lft_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt
let _P = λ_x 0
let _bin = λ__size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt λ_key λ_val λ_lft
let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft) _rgt.lft)
let _a = (((((((Book.BBT.new_node) _K) _V) _rgt.key) _rgt.val) _b) _rgt.rgt)
_a
let _tip = λ_key λ_val λ_lft ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) _lft) (((Book.BBT.tip) _K) _V))
((((((_rgt _P) _bin) _tip) _key) _val) _lft)
Book.BBT.new_node = λ_K λ_V λ_key λ_val λ_lft λ_rgt
let _P = λ_x (((Book.BBT) _K) _V)
let _new = λ_lft.size λ_lft
let _P = λ_x (((Book.BBT) _K) _V)
let _new = λ_rgt.size λ_rgt
let _new_size = (+ 1 (((Book.U60.max) _rgt.size) _lft.size))
((((((((Book.BBT.bin) _K) _V) _new_size) _key) _val) _lft) _rgt)
((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new)
((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
Book.BBT.rgt_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt
let _P = λ_x 0
let _bin = λ__size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_key λ_val λ_rgt
let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft.rgt) _rgt)
let _a = (((((((Book.BBT.new_node) _K) _V) _lft.key) _lft.val) _lft.lft) _b)
_a
let _tip = λ_key λ_val λ_rgt ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) (((Book.BBT.tip) _K) _V)) _rgt)
((((((_lft _P) _bin) _tip) _key) _val) _rgt)
Book.BBT.set = λ_K λ_V λ_cmp λ_key λ_val λ_map
let _P = λ_x 0
let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt λ_key λ_val
let _P = λ_x 0
let _ltn = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _new_lft = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.lft)
(((((((((Book.BBT.balance) _K) _V) _cmp) _key) _next.key) _next.val) _new_lft) _next.rgt)
let _eql = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _val) _next.lft) _next.rgt)
let _gtn = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt
let _new_rgt = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.rgt)
(((((((((Book.BBT.balance) _K) _V) _cmp) _key) _next.key) _next.val) _next.lft) _new_rgt)
(((((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _key) _next.key) _next.val) _next.lft) _next.rgt)
let _tip = λ_key λ_val (((((Book.BBT.singleton) _K) _V) _key) _val)
(((((_map _P) _bin) _tip) _key) _val)
Book.BBT.singleton = λ_K λ_V λ_key λ_val ((((((((Book.BBT.bin) _K) _V) 1) _key) _val) (((Book.BBT.tip) _K) _V)) (((Book.BBT.tip) _K) _V))
Book.BBT.tip = λ_K λ_V λ_P λ_bin λ_tip _tip
Book.BBT.to_list = λ_K λ_V λ_map
let _P = λ_x ((Book.List) (((Book.Pair) _K) _V))
let _bin = λ_size λ_key λ_val λ_lft λ_rgt
let _lft = ((((Book.BBT.to_list) _K) _V) _lft)
let _rgt = ((((Book.BBT.to_list) _K) _V) _rgt)
let _pair = (((((Book.Pair.new) _K) _V) _key) _val)
let _list = ((((Book.List.cons) (((Book.Pair) _K) _V)) _pair) ((((Book.List.concat) (((Book.Pair) _K) _V)) _lft) _rgt))
_list
let _tip = ((Book.List.nil) (((Book.Pair) _K) _V))
(((_map _P) _bin) _tip)
Book.Bool.and = λ_a
let _P = λ_a 0
let _true = λ_b _b
let _false = λ_b (Book.Bool.false)
(((_a _P) _true) _false)
Book.Bool.false = λ_P λ_t λ_f _f
Book.Bool.if = λ_b λ_P λ_t λ_f (((_b λ_x _P) _t) _f)
Book.Bool = 0
Book.Bool.lemma.notnot = λ_b (((_b λ_x ((((Book.Equal) (Book.Bool)) ((Book.Bool.not) ((Book.Bool.not) _x))) _x)) (((Book.Equal.refl) (Book.Bool)) (Book.Bool.true))) (((Book.Equal.refl) (Book.Bool)) (Book.Bool.false)))
Book.Bool.match = λ_b λ_P λ_t λ_f (((_b _P) _t) _f)
Book.Bool.not = λ_x
let _P = λ_x (Book.Bool)
let _true = (Book.Bool.false)
let _false = (Book.Bool.true)
(((_x _P) _true) _false)
Book.Bool.or = λ_a
let _P = λ_a 0
let _true = λ_b (Book.Bool.true)
let _false = λ_b _b
(((_a _P) _true) _false)
Book.Bool.show = λ_x
let _P = λ_x (Book.String)
let _true = (Str "true")
let _false = (Str "false")
(((_x _P) _true) _false)
Book.Bool.true = λ_P λ_t λ_f _t
Book.Char.equal = (Book.U60.equal)
Book.Char.escapes = ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 98) 8)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 102) 12)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 110) 10)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 114) 13)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 116) 9)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 118) 11)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 92) 92)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 34) 34)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 48) 0)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 39) 39)) ((Book.List.nil) (((Book.Pair) (Book.Char)) (Book.Char)))))))))))))
Book.Char.is_between = λ_min λ_max λ_chr (((Book.Bool.and) ((Book.U60.to_bool) (>= _chr _min))) ((Book.U60.to_bool) (<= _chr _max)))
Book.Char.is_blank = λ_a (((Book.Bool.or) (((Book.Char.equal) _a) 10)) (((Book.Char.equal) _a) 32))
Book.Char.is_decimal = λ_a ((((Book.Char.is_between) 48) 57) _a)
Book.Char.is_name = λ_a (((Book.Bool.or) ((((Book.Char.is_between) 97) 122) _a)) (((Book.Bool.or) ((((Book.Char.is_between) 65) 90) _a)) (((Book.Bool.or) ((((Book.Char.is_between) 48) 57) _a)) (((Book.Bool.or) (((Book.Char.equal) 95) _a)) (((Book.Bool.or) (((Book.Char.equal) 46) _a)) (((Book.Bool.or) (((Book.Char.equal) 45) _a)) (Book.Bool.false)))))))
Book.Char.is_newline = λ_a (((Book.Char.equal) _a) 10)
Book.Char.is_oper = λ_a (((Book.Bool.or) (((Book.Char.equal) 43) _a)) (((Book.Bool.or) (((Book.Char.equal) 45) _a)) (((Book.Bool.or) (((Book.Char.equal) 42) _a)) (((Book.Bool.or) (((Book.Char.equal) 47) _a)) (((Book.Bool.or) (((Book.Char.equal) 37) _a)) (((Book.Bool.or) (((Book.Char.equal) 60) _a)) (((Book.Bool.or) (((Book.Char.equal) 62) _a)) (((Book.Bool.or) (((Book.Char.equal) 61) _a)) (((Book.Bool.or) (((Book.Char.equal) 38) _a)) (((Book.Bool.or) (((Book.Char.equal) 124) _a)) (((Book.Bool.or) (((Book.Char.equal) 94) _a)) (((Book.Bool.or) (((Book.Char.equal) 33) _a)) (((Book.Bool.or) (((Book.Char.equal) 126) _a)) (Book.Bool.false))))))))))))))
Book.Char.is_slash = λ_a (((Book.Char.equal) _a) 47)
Book.Char = 0
Book.Char.slash = 92
Book.Cmp.eql = λ_P λ_ltn λ_eql λ_gtn _eql
Book.Cmp.gtn = λ_P λ_ltn λ_eql λ_gtn _gtn
Book.Cmp.is_gtn = λ_cmp
let _P = λ_x (Book.Bool)
let _ltn = (Book.Bool.false)
let _eql = (Book.Bool.false)
let _gtn = (Book.Bool.true)
((((_cmp _P) _ltn) _eql) _gtn)
Book.Cmp = 0
Book.Cmp.ltn = λ_P λ_ltn λ_eql λ_gtn _ltn
Book.Empty.absurd = λ_e λ_P (_e λ_x _P)
Book.Empty = 0
Book.Equal.apply = λ_A λ_B λ_f λ_a λ_b λ_e ((_e λ_x ((((Book.Equal) _B) (_f _a)) (_f _x))) λ_P λ_x _x)
Book.Equal = λ_A λ_a λ_b 0
Book.Equal.refl = λ_A λ_a λ_P λ_p _p
Book.HVM.load = λ_A λ_file λ_cont (_cont (Book.String.nil))
Book.HVM.log = λ_A λ_B λ_msg λ_ret _ret
Book.HVM.print = λ_A λ_msg λ_ret _ret
Book.HVM.print.many = λ_A λ_msgs λ_ret
let _P = λ_x _A
let _cons = λ_msg λ_msgs ((((Book.HVM.print) _A) _msg) ((((Book.HVM.print.many) _A) _msgs) _ret))
let _nil = _ret
(((_msgs _P) _cons) _nil)
Book.HVM.save = λ_A λ_file λ_data λ_cont _cont
Book.Kind.Binder = (((Book.Pair) (Book.String)) (Book.Kind.Term))
Book.Kind.Binder.new = λ_nam λ_typ (((((Book.Pair.new) (Book.String)) (Book.Kind.Term)) _nam) _typ)
Book.Kind.Book.String.cons = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term)))
Book.Kind.Book.String = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term)))
Book.Kind.Book.String.nil = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term)))
Book.Kind.Book.get_refs.go = λ_book
let _P = λ_x ((Book.List.Concatenator) (Book.String))
let _cons = λ_head λ_tail
let _P = λ_x ((Book.List.Concatenator) (Book.String))
let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Term.get_refs.go) _head.snd) (((Book.Kind.Book.get_refs.go) _tail) _nil))
((_head _P) _new)
let _nil = λ_nil _nil
(((_book _P) _cons) _nil)
Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
Book.Kind.Book = ((Book.String.Map) (Book.Kind.Term))
Book.Kind.Book.parse = λ_code
let _P = λ_x (Book.Kind.Book)
let _done = λ_code λ_book _book
let _fail = λ_error ((Book.String.Map.new) (Book.Kind.Term))
(((((Book.Kind.Book.parser) _code) _P) _done) _fail)
Book.Kind.Book.parser = (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (Book.Parser.is_eof)) λ_is_eof
let _P = λ_x ((Book.Parser) (Book.Kind.Book))
let _true = (((Book.Parser.pure) (Book.Kind.Book)) ((Book.String.Map.new) (Book.Kind.Term)))
let _false = (((((Book.Parser.bind) (Book.String)) (Book.Kind.Book)) (Book.Parser.name)) λ_nam (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) (Str ":")))) λ_ann
let _P = λ_x ((Book.Parser) (Book.Kind.Book))
let _true = (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str ":"))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_typ (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str "="))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_val (((((Book.Parser.bind) (Book.Kind.Book)) (Book.Kind.Book)) (Book.Kind.Book.parser)) λ_book (((Book.Parser.pure) (Book.Kind.Book)) (((((Book.String.Map.set) (Book.Kind.Term)) _nam) (((Book.Kind.ann) (_val ((Book.List.nil) (Book.Kind.Binder)))) (_typ ((Book.List.nil) (Book.Kind.Binder))))) _book)))))))
let _false = (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str "="))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_val (((((Book.Parser.bind) (Book.Kind.Book)) (Book.Kind.Book)) (Book.Kind.Book.parser)) λ_book (((Book.Parser.pure) (Book.Kind.Book)) (((((Book.String.Map.set) (Book.Kind.Term)) _nam) (_val ((Book.List.nil) (Book.Kind.Binder)))) _book)))))
(((_ann _P) _true) _false)))
(((_is_eof _P) _true) _false))
Book.Kind.Book.show.go = λ_book
let _P = λ_x (Book.String.Concatenator)
let _cons = λ_head λ_tail
let _P = λ_x (Book.String.Concatenator)
let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Text.show.go) _head.fst) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _head.snd) (Book.Nat.zero)) (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Book.show.go) _tail) _nil)))))
((_head _P) _new)
let _nil = λ_nil _nil
(((_book _P) _cons) _nil)
Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
Book.Kind.Book.to_hvm.go = λ_book
let _P = λ_x (Book.String.Concatenator)
let _cons = λ_head λ_tail
let _P = λ_x (Book.String.Concatenator)
let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Text.show.go) (Str "Book.")) (((Book.Kind.Text.show.go) _head.fst) (((Book.Kind.Text.show.go) (Str " = ")) ((((((Book.Kind.Term.to_hvm.go) _head.snd) (Book.Nat.zero)) (Book.Bool.true)) (Book.Nat.zero)) (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Book.to_hvm.go) _tail) _nil))))))
((_head _P) _new)
let _nil = λ_nil _nil
(((_book _P) _cons) _nil)
Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
Book.Kind.Oper.add = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _add
Book.Kind.Oper.and = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _and
Book.Kind.Oper.div = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _div
Book.Kind.Oper.eq = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _eq
Book.Kind.Oper.gt = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _gt
Book.Kind.Oper.gte = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _gte
Book.Kind.Oper = 0
Book.Kind.Oper.lsh = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lsh
Book.Kind.Oper.lt = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lt
Book.Kind.Oper.lte = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lte
Book.Kind.Oper.mod = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _mod
Book.Kind.Oper.mul = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _mul
Book.Kind.Oper.ne = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _ne
Book.Kind.Oper.or = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _or
Book.Kind.Oper.parser =
let _TRY = ((Book.List.cons) ((Book.Parser.Guard) (Book.Kind.Oper)))
let _END = ((Book.List.nil) ((Book.Parser.Guard) (Book.Kind.Oper)))
let _OP2 = λ_sym λ_oper ((((Book.Parser.Guard.text) (Book.Kind.Oper)) _sym) (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Oper)) ((Book.Parser.text) _sym)) λ_x (((Book.Parser.pure) (Book.Kind.Oper)) _oper)))
(((Book.Parser.variant) (Book.Kind.Oper)) ((_TRY ((_OP2 (Str "+")) (Book.Kind.Oper.add))) ((_TRY ((_OP2 (Str "*")) (Book.Kind.Oper.mul))) ((_TRY ((_OP2 (Str "-")) (Book.Kind.Oper.sub))) ((_TRY ((_OP2 (Str "/")) (Book.Kind.Oper.div))) ((_TRY ((_OP2 (Str "%")) (Book.Kind.Oper.mod))) ((_TRY ((_OP2 (Str "==")) (Book.Kind.Oper.eq))) ((_TRY ((_OP2 (Str "!=")) (Book.Kind.Oper.ne))) ((_TRY ((_OP2 (Str "<=")) (Book.Kind.Oper.lte))) ((_TRY ((_OP2 (Str ">=")) (Book.Kind.Oper.gte))) ((_TRY ((_OP2 (Str "<<")) (Book.Kind.Oper.lsh))) ((_TRY ((_OP2 (Str ">>")) (Book.Kind.Oper.rsh))) ((_TRY ((_OP2 (Str "<")) (Book.Kind.Oper.lt))) ((_TRY ((_OP2 (Str ">")) (Book.Kind.Oper.gt))) ((_TRY ((_OP2 (Str "&")) (Book.Kind.Oper.and))) ((_TRY ((_OP2 (Str "|")) (Book.Kind.Oper.or))) ((_TRY ((_OP2 (Str "^")) (Book.Kind.Oper.xor))) _END)))))))))))))))))
Book.Kind.Oper.rsh = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _rsh
Book.Kind.Oper.show.go = λ_oper
let _P = λ_X (Book.String.Concatenator)
let _add = ((Book.Kind.Text.show.go) (Str "+"))
let _mul = ((Book.Kind.Text.show.go) (Str "*"))
let _sub = ((Book.Kind.Text.show.go) (Str "-"))
let _div = ((Book.Kind.Text.show.go) (Str "/"))
let _mod = ((Book.Kind.Text.show.go) (Str "%"))
let _eq = ((Book.Kind.Text.show.go) (Str "=="))
let _ne = ((Book.Kind.Text.show.go) (Str "!="))
let _lt = ((Book.Kind.Text.show.go) (Str "<"))
let _gt = ((Book.Kind.Text.show.go) (Str ">"))
let _lte = ((Book.Kind.Text.show.go) (Str "<="))
let _gte = ((Book.Kind.Text.show.go) (Str ">="))
let _and = ((Book.Kind.Text.show.go) (Str "&"))
let _or = ((Book.Kind.Text.show.go) (Str "|"))
let _xor = ((Book.Kind.Text.show.go) (Str "^"))
let _lsh = ((Book.Kind.Text.show.go) (Str "<<"))
let _rsh = ((Book.Kind.Text.show.go) (Str ">>"))
(((((((((((((((((_oper _P) _add) _mul) _sub) _div) _mod) _eq) _ne) _lt) _gt) _lte) _gte) _and) _or) _xor) _lsh) _rsh)
Book.Kind.Oper.show = λ_oper ((Book.String.Concatenator.build) ((Book.Kind.Oper.show.go) _oper))
Book.Kind.Oper.sub = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _sub
Book.Kind.Oper.xor = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _xor
Book.Kind.PreTerm = 0
Book.Kind.Scope.cons = ((Book.List.cons) (Book.Kind.Binder))
Book.Kind.Scope.extend = λ_nam λ_typ λ_scp (((Book.Kind.Scope.cons) (((Book.Kind.Binder.new) _nam) _typ)) _scp)
Book.Kind.Scope.find = λ_name λ_scope
let _cond = λ_bnd ((_bnd λ_x (Book.Bool)) λ_n λ_t (((Book.String.equal) _name) _n))
let _found = ((((Book.List.find) (Book.Kind.Binder)) _cond) _scope)
let _P = λ_x (Book.Kind.Term)
let _some = λ_bnd ((_bnd λ_x (Book.Kind.Term)) λ_n λ_t _t)
let _none = (((Book.Kind.ref) _name) (Book.Kind.set))
(((_found _P) _some) _none)
Book.Kind.Scope = ((Book.List) (Book.Kind.Binder))
Book.Kind.Scope.nil = ((Book.List.nil) (Book.Kind.Binder))
Book.Kind.Term.get_refs.go = λ_term
let _P = λ_x ((Book.List.Concatenator) (Book.String))
let _all = λ_nam λ_inp λ_bod λ_nil (((Book.Kind.Term.get_refs.go) _inp) (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil))
let _lam = λ_nam λ_bod λ_nil (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil)
let _app = λ_fun λ_arg λ_nil (((Book.Kind.Term.get_refs.go) _fun) (((Book.Kind.Term.get_refs.go) _arg) _nil))
let _ann = λ_val λ_typ λ_nil (((Book.Kind.Term.get_refs.go) _val) (((Book.Kind.Term.get_refs.go) _typ) _nil))
let _slf = λ_nam λ_bod λ_nil (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil)
let _ins = λ_val λ_nil (((Book.Kind.Term.get_refs.go) _val) _nil)
let _ref = λ_nam λ_val λ_nil ((((Book.List.cons) (Book.String)) _nam) _nil)
let _def = λ_nam λ_val λ_bod λ_nil (((Book.Kind.Term.get_refs.go) _val) (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil))
let _set = λ_nil _nil
let _u60 = λ_nil _nil
let _num = λ_val λ_nil _nil
let _op2 = λ_opr λ_fst λ_snd λ_nil (((Book.Kind.Term.get_refs.go) _fst) (((Book.Kind.Term.get_refs.go) _snd) _nil))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil (((Book.Kind.Term.get_refs.go) _x) (((Book.Kind.Term.get_refs.go) _z) (((Book.Kind.Term.get_refs.go) (_s (Book.Kind.set))) (((Book.Kind.Term.get_refs.go) (_p (Book.Kind.set))) _nil))))
let _txt = λ_text λ_nil _nil
let _hol = λ_nam λ_ctx λ_nil _nil
let _var = λ_nam λ_idx λ_nil _nil
(((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.Term.get_refs = λ_term (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Term.get_refs.go) _term))
Book.Kind.Term = 0
Book.Kind.Term.parse = λ_code
let _P = λ_x (Book.Kind.Term)
let _done = λ_code λ_term (_term ((Book.List.nil) (Book.Kind.Binder)))
let _fail = λ_error (((Book.Kind.hol) (Str "error")) ((Book.List.nil) (Book.Kind.Term)))
(((((Book.Kind.Term.parser) _code) _P) _done) _fail)
Book.Kind.Term.parser.all = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "∀")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "∀"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_inp ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.all) _nam) (_inp _scp)) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp))))))))))))
Book.Kind.Term.parser.ann = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "{")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "{"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_typ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "}"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.ann) (_val _scp)) (_typ _scp)))))))))
Book.Kind.Term.parser.app = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "(")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_fun ((((Book.Kind.Term.parser.bind) ((Book.List) (Book.Kind.PreTerm))) ((((Book.Parser.until) (Book.Kind.PreTerm)) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) (Str ")")))) (Book.Kind.Term.parser))) λ_terms ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (((((((Book.List.fold) (Book.Kind.PreTerm)) _terms) 0) λ_arg λ_rec λ_fun (_rec (((Book.Kind.app) _fun) (_arg _scp)))) λ_fun _fun) (_fun _scp))))))))
Book.Kind.Term.parser.bind = λ_A (((Book.Parser.bind) _A) (Book.Kind.PreTerm))
Book.Kind.Term.parser.chr = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "'")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "'"))) λ__ ((((Book.Kind.Term.parser.bind) 0) (Book.Parser.char)) λ_chr ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "'"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.num) _chr))))))
Book.Kind.Term.parser.def = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "let ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "let "))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "="))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.def) _nam) (_val _scp)) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp))))))))))
Book.Kind.Term.parser.hol = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "?")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "?"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.hol) _nam) ((Book.List.nil) (Book.Kind.Term)))))))
Book.Kind.Term.parser.ins = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "~")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "~"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.ins) (_val _scp))))))
Book.Kind.Term.parser =
let _TRY = ((Book.List.cons) ((Book.Parser.Guard) (Book.Kind.PreTerm)))
let _END = ((Book.List.nil) ((Book.Parser.Guard) (Book.Kind.PreTerm)))
(((Book.Parser.variant) (Book.Kind.PreTerm)) ((_TRY (Book.Kind.Term.parser.all)) ((_TRY (Book.Kind.Term.parser.lam)) ((_TRY (Book.Kind.Term.parser.app)) ((_TRY (Book.Kind.Term.parser.ann)) ((_TRY (Book.Kind.Term.parser.slf)) ((_TRY (Book.Kind.Term.parser.ins)) ((_TRY (Book.Kind.Term.parser.set)) ((_TRY (Book.Kind.Term.parser.def)) ((_TRY (Book.Kind.Term.parser.u60)) ((_TRY (Book.Kind.Term.parser.op2)) ((_TRY (Book.Kind.Term.parser.mat)) ((_TRY (Book.Kind.Term.parser.chr)) ((_TRY (Book.Kind.Term.parser.str)) ((_TRY (Book.Kind.Term.parser.num)) ((_TRY (Book.Kind.Term.parser.hol)) ((_TRY (Book.Kind.Term.parser.var)) _END)))))))))))))))))
Book.Kind.Term.parser.lam = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "λ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "λ"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.lam) _nam) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp))))))))
Book.Kind.Term.parser.mat = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#match ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#match "))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "="))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_x ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "{"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#0"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_z ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#+"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_s ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "}"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_p ((Book.Kind.Term.parser.pure) λ_scp ((((((Book.Kind.mat) _nam) (_x _scp)) (_z _scp)) λ_x (_s ((((Book.Kind.Scope.extend) (((Book.String.concat) _nam) (Str "-1"))) _x) _scp))) λ_x (_p ((((Book.Kind.Scope.extend) _nam) _x) _scp)))))))))))))))))))
Book.Kind.Term.parser.num = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#"))) λ__ ((((Book.Kind.Term.parser.bind) 0) (Book.U60.parser.decimal)) λ_num ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.num) _num)))))
Book.Kind.Term.parser.op2 = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#(")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.Oper)) (Book.Kind.Oper.parser)) λ_opr ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_fst ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_snd ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.op2) _opr) (_fst _scp)) (_snd _scp)))))))))
Book.Kind.Term.parser.pure = ((Book.Parser.pure) (Book.Kind.PreTerm))
Book.Kind.Term.parser.set = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "*")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "*"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (Book.Kind.set))))
Book.Kind.Term.parser.slf = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "$")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "$"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.slf) _nam) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp))))))))
Book.Kind.Term.parser.str = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Book.String.quote)) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Book.String.quote))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) ((((Book.Parser.until) (Book.Char)) ((Book.Parser.test) (Book.String.quote))) (Book.Parser.char))) λ_chars ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Book.String.quote))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.txt) _chars))))))
Book.Kind.Term.parser.u60 = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#U60")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#U60"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (Book.Kind.u60))))
Book.Kind.Term.parser.var = (((Book.Parser.Guard.pass) (Book.Kind.PreTerm)) ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.Scope.find) _nam) _scp))))
Book.Kind.Term.show.go = λ_term λ_dep
let _P = λ_X (Book.String.Concatenator)
let _all = λ_nam λ_inp λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "∀(")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str ": ")) ((((Book.Kind.Term.show.go) _inp) _dep) (((Book.Kind.Text.show.go) (Str ") ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil))))))
let _lam = λ_nam λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil))))
let _app = λ_fun λ_arg λ_nil (((Book.Kind.Text.show.go) (Str "(")) ((((Book.Kind.Term.show.go) _fun) _dep) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _arg) _dep) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))
let _ann = λ_val λ_typ λ_nil (((Book.Kind.Text.show.go) (Str "{")) ((((Book.Kind.Term.show.go) _val) _dep) (((Book.Kind.Text.show.go) (Str " : ")) ((((Book.Kind.Term.show.go) _typ) _dep) (((Book.Kind.Text.show.go) (Str "}")) _nil)))))
let _slf = λ_nam λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "$")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil))))
let _ins = λ_val λ_nil (((Book.Kind.Text.show.go) (Str "~")) ((((Book.Kind.Term.show.go) _val) _dep) _nil))
let _ref = λ_nam λ_val λ_nil (((Book.Kind.Text.show.go) _nam) _nil)
let _def = λ_nam λ_val λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "let ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _val) _dep) (((Book.Kind.Text.show.go) (Str "; ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil))))))
let _set = λ_nil (((Book.Kind.Text.show.go) (Str "*")) _nil)
let _u60 = λ_nil (((Book.Kind.Text.show.go) (Str "#U60")) _nil)
let _num = λ_val λ_nil (((Book.Kind.Text.show.go) (Str "#")) (((Book.U60.show.go) _val) _nil))
let _op2 = λ_opr λ_fst λ_snd λ_nil (((Book.Kind.Text.show.go) (Str "#(")) (((Book.Kind.Oper.show.go) _opr) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _fst) _dep) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _snd) _dep) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil (((Book.Kind.Text.show.go) (Str "#match ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _x) _dep) (((Book.Kind.Text.show.go) (Str " { #0: ")) ((((Book.Kind.Term.show.go) _z) _dep) (((Book.Kind.Text.show.go) (Str "; #+: ")) ((((Book.Kind.Term.show.go) (_s (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep))) ((Book.Nat.succ) _dep)) (((Book.Kind.Text.show.go) (Str " }: ")) ((((Book.Kind.Term.show.go) (_p (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil))))))))))
let _txt = λ_text λ_nil (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) _text) (((Book.Kind.Text.show.go) (Book.String.quote)) _nil)))
let _hol = λ_nam λ_ctx λ_nil (((Book.Kind.Text.show.go) (Str "?")) (((Book.Kind.Text.show.go) _nam) _nil))
let _var = λ_nam λ_idx λ_nil (((Book.Kind.Text.show.go) _nam) _nil)
(((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.Term.show = λ_term λ_dep ((Book.String.Concatenator.build) (((Book.Kind.Term.show.go) _term) _dep))
Book.Kind.Term.to_hvm.go = λ_term λ_dep λ_inc λ_tab
let _P = λ_x (Book.String.Concatenator)
let _all = λ_nam λ_inp λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil))
let _lam = λ_nam λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.true)) _tab) _nil)))))
let _app = λ_fun λ_arg λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(")) ((((((Book.Kind.Term.to_hvm.go) _fun) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _arg) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) _nil))))))
let _ann = λ_val λ_typ λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) _nil))
let _slf = λ_nam λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil))
let _ins = λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) _nil))
let _ref = λ_nam λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(Book.")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str ")")) _nil))))
let _def = λ_nam λ_val λ_bod λ_nil
let _tab = ((((_inc λ_x 0) (Book.Nat.succ)) λ_x _x) _tab)
(((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Text.show.go) ((Book.String.indent) _tab)) (((Book.Kind.Text.show.go) (Str "let ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) (((Book.Kind.Text.show.go) (Str " = ")) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.false)) _tab) _nil))))))))
let _set = λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil))
let _u60 = λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil))
let _num = λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.U60.show.go) _val) _nil))
let _op2 = λ_opr λ_fst λ_snd λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(")) (((Book.Kind.Oper.show.go) _opr) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _fst) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _snd) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) _nil))))))))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(U60.match ")) ((((((Book.Kind.Term.to_hvm.go) _x) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _z) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) (((Book.String.concat) _nam) (Str "_1")))) (((Book.Kind.Text.show.go) (Str "(")) ((((((Book.Kind.Term.to_hvm.go) (_s (((Book.Kind.var) (((Book.String.concat) _nam) (Str "_1"))) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) (((Book.Kind.Text.show.go) (Str ")")) _nil))))))))))))
let _txt = λ_txt λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(Str ")) (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) _txt) (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) (Str ")")) _nil))))))
let _hol = λ_nam λ_ctx λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil))
let _var = λ_nam λ_idx λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) _nil))
(((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.Term.to_hvm = λ_term λ_dep ((Book.String.Concatenator.build) (((Book.Kind.Term.to_hvm.go) _term) _dep))
Book.Kind.Term.to_hvm.nl = λ_inc λ_tab
let _P = λ_x (Book.String.Concatenator)
let _true = λ_nil _nil
let _false = λ_nil (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Text.show.go) ((Book.String.indent) _tab)) _nil))
(((_inc _P) _true) _false)
Book.Kind.Text = (Book.String)
Book.Kind.Text.show.go = (Book.String.Concatenator.from_string)
Book.Kind.all = λ_nam λ_inp λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_all _nam) _inp) _bod)
Book.Kind.ann = λ_val λ_typ λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_ann _val) _typ)
Book.Kind.app = λ_fun λ_arg λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_app _fun) _arg)
Book.Kind.check = λ_term λ_type λ_dep
let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term))
let _pure = ((Book.Maybe.some) (Book.Kind.Term))
let _none = ((Book.Maybe.none) (Book.Kind.Term))
let _P = λ_x 0
let _all = λ_term.nam λ_term.inp λ_term.bod λ_type λ_dep ((((Book.Kind.verify) ((((Book.Kind.all) _term.nam) _term.inp) _term.bod)) _type) _dep)
let _lam = λ_term.nam λ_term.bod λ_type λ_dep (((((((Book.Kind.if.all) (((Book.Kind.reduce) (Book.Bool.true)) _type)) 0) λ_type.nam λ_type.inp λ_type.bod λ_dep λ_term.bod
let _ann = (((Book.Kind.ann) (((Book.Kind.var) _term.nam) _dep)) _type.inp)
let _term = (_term.bod _ann)
let _type = (_type.bod _ann)
((((Book.Kind.check) _term) _type) ((Book.Nat.succ) _dep))) λ_type λ_dep λ_term.bod (((Book.Kind.infer) (((Book.Kind.lam) _term.nam) _term.bod)) _dep)) _dep) _term.bod)
let _app = λ_term.fun λ_term.arg λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.app) _term.fun) _term.arg)) _type) _dep)
let _ann = λ_val λ_typ λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.ann) _val) _typ)) _type) _dep)
let _slf = λ_term.nam λ_term.bod λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.slf) _term.nam) _term.bod)) _type) _dep)
let _ins = λ_term.val λ_type λ_dep ((((((Book.Kind.if.slf) (((Book.Kind.reduce) (Book.Bool.true)) _type)) 0) λ_type.nam λ_type.bod λ_term.val ((((Book.Kind.check) _term.val) (_type.bod ((Book.Kind.ins) _term.val))) _dep)) λ_type λ_term.val (((Book.Kind.infer) ((Book.Kind.ins) _term.val)) _dep)) _term.val)
let _ref = λ_term.nam λ_term.val λ_type λ_dep ((((Book.Kind.check) _term.val) _type) _dep)
let _def = λ_term.nam λ_term.val λ_term.bod λ_type λ_dep ((((Book.Kind.check) (_term.bod _term.val)) _type) ((Book.Nat.succ) _dep))
let _set = λ_type λ_dep ((((Book.Kind.verify) (Book.Kind.set)) _type) _dep)
let _u60 = λ_type λ_dep ((((Book.Kind.verify) (Book.Kind.u60)) _type) _dep)
let _num = λ_term.num λ_type λ_dep ((((Book.Kind.verify) ((Book.Kind.num) _term.num)) _type) _dep)
let _op2 = λ_term.opr λ_term.fst λ_term.snd λ_type λ_dep ((((Book.Kind.verify) ((((Book.Kind.op2) _term.opr) _term.fst) _term.snd)) _type) _dep)
let _mat = λ_term.nam λ_term.x λ_term.z λ_term.s λ_term.p λ_type λ_dep ((((Book.Kind.verify) ((((((Book.Kind.mat) _term.nam) _term.x) _term.z) _term.s) _term.p)) _type) _dep)
let _txt = λ_term.txt λ_type λ_dep ((((Book.Kind.verify) ((Book.Kind.txt) _term.txt)) _type) _dep)
let _hol = λ_term.nam λ_term.ctx λ_type λ_dep (_pure (Book.Kind.set))
let _var = λ_term.nam λ_term.idx λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.var) _term.nam) _term.idx)) _type) _dep)
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _type) _dep)
Book.Kind.comparer = λ_rec λ_a λ_b λ_dep
let _VAR = (Book.Kind.var)
let _SUC = (Book.Nat.succ)
let _a = ((Book.Kind.skip) _a)
let _b = ((Book.Kind.skip) _b)
let _R = 0
let _Y = λ_a.nam λ_a.ctx λ_b λ_dep (Book.Bool.true)
let _N = λ_a λ_b λ_dep
let _R = 0
let _Y = λ_b.nam λ_b.ctx λ_dep λ_a (Book.Bool.true)
let _N = λ_b λ_dep λ_a
let _P = λ_x 0
let _all = λ_a.nam λ_a.inp λ_a.bod λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.inp λ_b.bod λ_dep (((Book.Bool.and) (((_rec _a.inp) _b.inp) _dep)) (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep)))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.all) _b) _P) _Y) _N) _dep)
let _lam = λ_a.nam λ_a.bod λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.bod λ_dep (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.lam) _b) _P) _Y) _N) _dep)
let _app = λ_a.fun λ_a.arg λ_b λ_dep
let _P = 0
let _Y = λ_b.fun λ_b.arg λ_dep (((Book.Bool.and) (((_rec _a.fun) _b.fun) _dep)) (((_rec _a.arg) _b.arg) _dep))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.app) _b) _P) _Y) _N) _dep)
let _ann = λ_a.val λ_a.typ λ_b λ_dep (Book.Bool.false)
let _slf = λ_a.nam λ_a.bod λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.bod λ_dep (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.slf) _b) _P) _Y) _N) _dep)
let _ins = λ_a.val λ_b λ_dep (Book.Bool.false)
let _ref = λ_a.nam λ_a.val λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.val λ_dep (((Book.String.equal) _a.nam) _b.nam)
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.ref) _b) _P) _Y) _N) _dep)
let _def = λ_a.nam λ_a.val λ_a.bod λ_b λ_dep (Book.Bool.false)
let _set = λ_b λ_dep
let _P = 0
let _Y = λ_dep (Book.Bool.true)
let _F = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.set) _b) _P) _Y) _F) _dep)
let _u60 = λ_b λ_dep
let _P = 0
let _Y = λ_dep (Book.Bool.true)
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.u60) _b) _P) _Y) _N) _dep)
let _num = λ_a.val λ_b λ_dep
let _P = 0
let _Y = λ_b.val λ_dep (((Book.U60.equal) _a.val) _b.val)
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.num) _b) _P) _Y) _N) _dep)
let _op2 = λ_a.opr λ_a.fst λ_a.snd λ_b λ_dep
let _P = 0
let _Y = λ_b.opr λ_b.fst λ_b.snd λ_dep (((Book.Bool.and) (((_rec _a.fst) _b.fst) _dep)) (((_rec _a.snd) _b.snd) _dep))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.op2) _b) _P) _Y) _N) _dep)
let _mat = λ_a.nam λ_a.x λ_a.z λ_a.s λ_a.p λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.x λ_b.z λ_b.s λ_b.p λ_dep (((Book.Bool.and) (((_rec _a.x) _b.x) _dep)) (((Book.Bool.and) (((_rec _a.z) _b.z) _dep)) (((Book.Bool.and) (((_rec (_a.s ((_VAR (((Book.String.concat) _a.nam) (Str "-1"))) _dep))) (_b.s ((_VAR (((Book.String.concat) _b.nam) (Str "-1"))) _dep))) (_SUC _dep))) (((_rec (_a.p ((_VAR _a.nam) _dep))) (_b.p ((_VAR _b.nam) _dep))) (_SUC _dep)))))
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.mat) _b) _P) _Y) _N) _dep)
let _txt = λ_a.txt λ_b λ_dep
let _P = 0
let _Y = λ_b.txt λ_dep (((Book.String.equal) _a.txt) _b.txt)
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.txt) _b) _P) _Y) _N) _dep)
let _hol = λ_a.nam λ_a.ctx λ_b λ_dep (Book.Bool.false)
let _var = λ_a.nam λ_a.idx λ_b λ_dep
let _P = 0
let _Y = λ_b.nam λ_b.idx λ_dep (((Book.Nat.equal) _a.idx) _b.idx)
let _N = λ_val λ_dep (Book.Bool.false)
((((((Book.Kind.if.var) _b) _P) _Y) _N) _dep)
(((((((((((((((((((_a _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _b) _dep)
(((((((Book.Kind.if.hol) _b) _R) _Y) _N) _dep) _a)
(((((((Book.Kind.if.hol) _a) _R) _Y) _N) _b) _dep)
Book.Kind.def = λ_nam λ_val λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_def _nam) _val) _bod)
Book.Kind.equal.enter = λ_e λ_a λ_b λ_dep
let _P = λ_x 0
let _true = λ_a λ_b λ_dep (Book.Bool.true)
let _false = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.equal)) _a) _b) _dep)
((((((_e _P) _true) _false) _a) _b) _dep)
Book.Kind.equal = λ_a λ_b λ_dep (((((Book.Kind.equal.minor) ((((Book.Kind.identical) _a) _b) _dep)) _a) _b) _dep)
Book.Kind.equal.major = λ_e λ_a λ_b λ_dep
let _P = λ_x 0
let _true = λ_a λ_b λ_dep (Book.Bool.true)
let _false = λ_a λ_b λ_dep
let _a_wnf = (((Book.Kind.reduce) (Book.Bool.true)) _a)
let _b_wnf = (((Book.Kind.reduce) (Book.Bool.true)) _b)
(((((Book.Kind.equal.enter) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep)
((((((_e _P) _true) _false) _a) _b) _dep)
Book.Kind.equal.minor = λ_e λ_a λ_b λ_dep
let _P = λ_x 0
let _true = λ_a λ_b λ_dep (Book.Bool.true)
let _false = λ_a λ_b λ_dep
let _a_wnf = (((Book.Kind.reduce) (Book.Bool.false)) _a)
let _b_wnf = (((Book.Kind.reduce) (Book.Bool.false)) _b)
(((((Book.Kind.equal.major) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep)
((((((_e _P) _true) _false) _a) _b) _dep)
Book.Kind.hol = λ_nam λ_ctx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_hol _nam) _ctx)
Book.Kind.identical = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.identical)) _a) _b) _dep)
Book.Kind.if.all = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (((_Y _nam) _inp) _bod)
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.ann = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N ((_Y _val) _typ)
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.app = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N ((_Y _fun) _arg)
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.def = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (((_Y _nam) _val) _bod)
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.hol = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N ((_Y _nam) _ctx)
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.ins = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_Y _val)
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.lam = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N ((_Y _nam) _bod)
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.mat = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (((((_Y _nam) _x) _z) _s) _p)
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.num = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_Y _val)
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.op2 = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (((_Y _opr) _fst) _snd)
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.ref = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N ((_Y _nam) _val)
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.set = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N _Y
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.slf = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N ((_Y _nam) _bod)
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.txt = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_Y _lit)
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.u60 = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N _Y
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx))
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.if.var = λ_term λ_P λ_Y λ_N
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod))
let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod))
let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg))
let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ))
let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod))
let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val))
let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val))
let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod))
let _set = λ_Y λ_N (_N (Book.Kind.set))
let _u60 = λ_Y λ_N (_N (Book.Kind.u60))
let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val))
let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p))
let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit))
let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx))
let _var = λ_nam λ_idx λ_Y λ_N ((_Y _nam) _idx)
(((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N)
Book.Kind.infer = λ_term λ_dep
let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term))
let _pure = ((Book.Maybe.some) (Book.Kind.Term))
let _none = ((Book.Maybe.none) (Book.Kind.Term))
let _P = λ_x 0
let _all = λ_nam λ_inp λ_bod λ_dep ((_bind ((((Book.Kind.check) _inp) (Book.Kind.set)) _dep)) λ__ ((_bind ((((Book.Kind.check) (_bod (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) _inp))) (Book.Kind.set)) ((Book.Nat.succ) _dep))) λ__ (_pure (Book.Kind.set))))
let _lam = λ_nam λ_bod λ_dep _none
let _app = λ_fun λ_arg λ_dep ((_bind (((Book.Kind.infer) _fun) _dep)) λ_fun_typ (((((((Book.Kind.if.all) (((Book.Kind.reduce) (Book.Bool.true)) _fun_typ)) 0) λ_fun_typ.nam λ_fun_typ.inp λ_fun_typ.bod λ_fun λ_arg ((_bind ((((Book.Kind.check) _arg) _fun_typ.inp) _dep)) λ__ (_pure (_fun_typ.bod _arg)))) λ_fun_typ λ_fun λ_arg _none) _fun) _arg))
let _ann = λ_val λ_typ λ_dep (_pure _typ)
let _slf = λ_nam λ_bod λ_dep ((_bind ((((Book.Kind.check) (_bod (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) (((Book.Kind.slf) _nam) _bod)))) (Book.Kind.set)) ((Book.Nat.succ) _dep))) λ__ (_pure (Book.Kind.set)))
let _ins = λ_val λ_dep ((_bind (((Book.Kind.infer) _val) _dep)) λ_val_typ ((((((Book.Kind.if.slf) (((Book.Kind.reduce) (Book.Bool.true)) _val_typ)) 0) λ_val_nam λ_val_typ.bod λ_val (_pure (_val_typ.bod ((Book.Kind.ins) _val)))) λ_val_typ λ_val _none) _val))
let _ref = λ_nam λ_val λ_dep (((Book.Kind.infer) _val) _dep)
let _def = λ_nam λ_val λ_bod λ_dep _none
let _set = λ_dep (_pure (Book.Kind.set))
let _u60 = λ_dep (_pure (Book.Kind.set))
let _num = λ_num λ_dep (_pure (Book.Kind.u60))
let _txt = λ_txt λ_dep (_pure (Book.Kind.Book.String))
let _op2 = λ_opr λ_fst λ_snd λ_dep ((_bind ((((Book.Kind.check) _fst) (Book.Kind.u60)) _dep)) λ__ ((_bind ((((Book.Kind.check) _snd) (Book.Kind.u60)) _dep)) λ__ (_pure (Book.Kind.u60))))
let _mat = λ_nam λ_x λ_z λ_s λ_p λ_dep ((_bind ((((Book.Kind.check) _x) (Book.Kind.u60)) _dep)) λ_x_typ ((_bind ((((Book.Kind.check) (_p (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) (Book.Kind.u60)))) (Book.Kind.set)) _dep)) λ_p_typ ((_bind ((((Book.Kind.check) _z) (_p ((Book.Kind.num) 0))) _dep)) λ_z_typ ((_bind ((((Book.Kind.check) (_s (((Book.Kind.ann) (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep)) (Book.Kind.u60)))) (_p ((((Book.Kind.op2) (Book.Kind.Oper.add)) ((Book.Kind.num) 1)) (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep)))) ((Book.Nat.succ) _dep))) λ_s_typ (_pure (_p _x))))))
let _hol = λ_nam λ_ctx λ_dep _none
let _var = λ_nam λ_idx λ_dep _none
((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _dep)
Book.Kind.ins = λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_ins _val)
Book.Kind =
let _a = (((Book.Kind.lam) (Str "f")) λ_f (((Book.Kind.lam) (Str "x")) λ_x (((Book.Kind.app) _f) (((Book.Kind.app) _f) _x))))
let _b = (((Book.Kind.lam) (Str "f")) λ_f (((Book.Kind.lam) (Str "x")) λ_x (((Book.Kind.app) _f) (((Book.Kind.app) _f) _x))))
let _Test = ((((Book.Kind.all) (Str "A")) (Book.Kind.set)) λ_A ((((Book.Kind.all) (Str "B")) (Book.Kind.set)) λ_B ((((Book.Kind.all) (Str "a")) _A) λ_a ((((Book.Kind.all) (Str "b")) _B) λ_b _B))))
let _test = (((Book.Kind.lam) (Str "A")) λ_A (((Book.Kind.lam) (Str "B")) λ_B (((Book.Kind.lam) (Str "a")) λ_a (((Book.Kind.lam) (Str "b")) λ_b _b))))
let _P = λ_x (Book.String)
let _some = λ_value (((Book.Kind.Term.show) _value) (Book.Nat.zero))
let _none = (Str "error")
let _chk = ((((Book.Kind.check) _test) _Test) (Book.Nat.zero))
(((_chk _P) _some) _none)
Book.Kind.lam = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_lam _nam) _bod)
Book.Kind.mat = λ_nam λ_x λ_z λ_s λ_p λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((((_mat _nam) _x) _z) _s) _p)
Book.Kind.normal.go = λ_maj λ_term λ_dep
let _P = λ_x (Book.Kind.Term)
let _all = λ_nam λ_inp λ_bod ((((Book.Kind.all) _nam) ((((Book.Kind.normal) _maj) _inp) _dep)) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)))
let _lam = λ_nam λ_bod (((Book.Kind.lam) _nam) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)))
let _app = λ_fun λ_arg (((Book.Kind.app) ((((Book.Kind.normal) _maj) _fun) _dep)) ((((Book.Kind.normal) _maj) _arg) _dep))
let _ann = λ_val λ_typ (((Book.Kind.ann) ((((Book.Kind.normal) _maj) _val) _dep)) ((((Book.Kind.normal) _maj) _typ) _dep))
let _slf = λ_nam λ_bod (((Book.Kind.slf) _nam) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)))
let _ins = λ_val ((Book.Kind.ins) ((((Book.Kind.normal) _maj) _val) _dep))
let _ref = λ_nam λ_val (((Book.Kind.ref) _nam) ((((Book.Kind.normal) _maj) _val) _dep))
let _def = λ_nam λ_val λ_bod ((((Book.Kind.def) _nam) ((((Book.Kind.normal) _maj) _val) _dep)) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)))
let _set = (Book.Kind.set)
let _u60 = (Book.Kind.u60)
let _num = (Book.Kind.num)
let _op2 = λ_opr λ_fst λ_snd ((((Book.Kind.op2) _opr) ((((Book.Kind.normal) _maj) _fst) _dep)) ((((Book.Kind.normal) _maj) _snd) _dep))
let _mat = λ_nam λ_x λ_z λ_s λ_p ((((((Book.Kind.mat) _nam) ((((Book.Kind.normal) _maj) _x) _dep)) ((((Book.Kind.normal) _maj) _z) _dep)) λ_k ((((Book.Kind.normal) _maj) (_s (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) λ_k ((((Book.Kind.normal) _maj) (_p (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)))
let _txt = λ_txt ((Book.Kind.txt) _txt)
let _hol = λ_nam λ_ctx (((Book.Kind.hol) _nam) _ctx)
let _var = λ_nam λ_idx (((Book.Kind.var) _nam) _idx)
(((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.normal = λ_maj λ_term λ_dep ((((Book.Kind.normal.go) _maj) (((Book.Kind.reduce) _maj) _term)) _dep)
Book.Kind.num = λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_num _val)
Book.Kind.op2 = λ_opr λ_fst λ_snd λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_op2 _opr) _fst) _snd)
Book.Kind.reduce.app = λ_maj λ_fun λ_arg
let _P = 0
let _Y = λ_nam λ_bod λ_arg (((Book.Kind.reduce) _maj) (_bod (((Book.Kind.reduce) _maj) _arg)))
let _N = λ_fun λ_arg (((Book.Kind.app) _fun) _arg)
((((((Book.Kind.if.lam) _fun) _P) _Y) _N) _arg)
Book.Kind.reduce = λ_maj λ_term
let _P = λ_x (Book.Kind.Term)
let _all = (Book.Kind.all)
let _lam = (Book.Kind.lam)
let _app = λ_fun λ_arg ((((Book.Kind.reduce.app) _maj) (((Book.Kind.reduce) _maj) _fun)) _arg)
let _slf = (Book.Kind.slf)
let _ann = λ_val λ_typ (((Book.Kind.reduce) _maj) _val)
let _ins = λ_val (((Book.Kind.reduce) _maj) _val)
let _ref = λ_nam λ_val ((((Book.Kind.reduce.ref) _maj) _nam) _val)
let _def = λ_nam λ_val λ_bod (((Book.Kind.reduce) _maj) (_bod _val))
let _set = (Book.Kind.set)
let _u60 = (Book.Kind.u60)
let _num = (Book.Kind.num)
let _op2 = λ_opr λ_fst λ_snd ((((Book.Kind.reduce.op2) _opr) _fst) _snd)
let _mat = λ_nam λ_x λ_z λ_s λ_p (((((((Book.Kind.reduce.mat) _maj) _nam) _x) _z) _s) _p)
let _txt = λ_txt ((Book.Kind.reduce.txt) _txt)
let _hol = (Book.Kind.hol)
let _var = (Book.Kind.var)
(((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.reduce.mat = λ_maj λ_nam λ_x λ_z λ_s λ_p
let _P = 0
let _Y = λ_x.val (U60.match _x.val λ_z λ_s (((Book.Kind.reduce) _maj) _z) λ_x_1(λ_z λ_s (((Book.Kind.reduce) _maj) (_s ((Book.Kind.num) _x_1)))))
let _N = λ_x λ_z λ_s ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)
(((((((Book.Kind.if.num) _x) _P) _Y) _N) _z) _s)
Book.Kind.reduce.op2 = λ_opr λ_fst λ_snd
let _P = 0
let _Y = λ_fst_val λ_snd
let _P = 0
let _Y = λ_snd_val λ_fst_val
let _P = λ_x 0
let _add = λ_fst_val λ_snd_val ((Book.Kind.num) (+ _fst_val _snd_val))
let _mul = λ_fst_val λ_snd_val ((Book.Kind.num) (* _fst_val _snd_val))
let _sub = λ_fst_val λ_snd_val ((Book.Kind.num) (- _fst_val _snd_val))
let _div = λ_fst_val λ_snd_val ((Book.Kind.num) (/ _fst_val _snd_val))
let _eq = λ_fst_val λ_snd_val ((Book.Kind.num) (== _fst_val _snd_val))
let _ne = λ_fst_val λ_snd_val ((Book.Kind.num) (!= _fst_val _snd_val))
let _lt = λ_fst_val λ_snd_val ((Book.Kind.num) (< _fst_val _snd_val))
let _gt = λ_fst_val λ_snd_val ((Book.Kind.num) (> _fst_val _snd_val))
let _lte = λ_fst_val λ_snd_val ((Book.Kind.num) (<= _fst_val _snd_val))
let _gte = λ_fst_val λ_snd_val ((Book.Kind.num) (>= _fst_val _snd_val))
let _and = λ_fst_val λ_snd_val ((Book.Kind.num) (& _fst_val _snd_val))
let _or = λ_fst_val λ_snd_val ((Book.Kind.num) (| _fst_val _snd_val))
let _xor = λ_fst_val λ_snd_val ((Book.Kind.num) (^ _fst_val _snd_val))
let _lsh = λ_fst_val λ_snd_val ((Book.Kind.num) (<< _fst_val _snd_val))
let _rsh = λ_fst_val λ_snd_val ((Book.Kind.num) (>> _fst_val _snd_val))
((((((((((((((((((_opr _P) _add) _mul) _sub) _div) _eq) _ne) _lt) _gt) _lte) _gte) _and) _or) _xor) _lsh) _rsh) _fst_val) _snd_val)
let _N = λ_snd λ_fst_val ((((Book.Kind.op2) _opr) ((Book.Kind.num) _fst_val)) _snd)
((((((Book.Kind.if.num) _snd) _P) _Y) _N) _fst_val)
let _N = λ_fst λ_snd ((((Book.Kind.op2) _opr) _fst) _snd)
((((((Book.Kind.if.num) _fst) _P) _Y) _N) _snd)
Book.Kind.reduce.ref = λ_maj λ_nam λ_val
let _P = λ_x 0
let _true = λ_nam λ_val (((Book.Kind.reduce) _maj) _val)
let _false = (Book.Kind.ref)
(((((_maj _P) _true) _false) _nam) _val)
Book.Kind.reduce.txt = λ_txt
let _P = λ_x (Book.Kind.Term)
let _cons = λ_x λ_xs (((Book.Kind.reduce) (Book.Bool.true)) (((Book.Kind.app) (((Book.Kind.app) (Book.Kind.Book.String.cons)) ((Book.Kind.num) _x))) ((Book.Kind.txt) _xs)))
let _nil = (((Book.Kind.reduce) (Book.Bool.true)) (Book.Kind.Book.String.nil))
(((_txt _P) _cons) _nil)
Book.Kind.ref = λ_nam λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_ref _nam) _val)
Book.Kind.report = λ_e λ_inferred λ_expected λ_value λ_dep
let _pure = ((Book.Maybe.some) (Book.Kind.Term))
let _none = ((Book.Maybe.none) (Book.Kind.Term))
let _P = λ_x 0
let _true = λ_inferred λ_expected λ_value λ_dep (_pure (Book.Kind.set))
let _false = λ_inferred λ_expected λ_value λ_dep _none
(((((((_e _P) _true) _false) _inferred) _expected) _value) _dep)
Book.Kind.set = λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var _set
Book.Kind.skip = λ_x
let _P = λ_x (Book.Kind.Term)
let _all = (Book.Kind.all)
let _lam = (Book.Kind.lam)
let _app = (Book.Kind.app)
let _ann = λ_val λ_typ ((Book.Kind.skip) _val)
let _slf = (Book.Kind.slf)
let _ins = λ_val ((Book.Kind.skip) _val)
let _ref = (Book.Kind.ref)
let _def = λ_nam λ_val λ_bod ((Book.Kind.skip) (_bod _val))
let _set = (Book.Kind.set)
let _u60 = (Book.Kind.u60)
let _num = (Book.Kind.num)
let _op2 = (Book.Kind.op2)
let _mat = (Book.Kind.mat)
let _txt = (Book.Kind.txt)
let _hol = (Book.Kind.hol)
let _var = (Book.Kind.var)
(((((((((((((((((_x _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var)
Book.Kind.slf = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_slf _nam) _bod)
Book.Kind.txt = λ_lit λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_txt _lit)
Book.Kind.u60 = λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var _u60
Book.Kind.var = λ_nam λ_idx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_var _nam) _idx)
Book.Kind.verify = λ_term λ_type λ_dep
let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term))
let _pure = ((Book.Maybe.some) (Book.Kind.Term))
let _none = ((Book.Maybe.none) (Book.Kind.Term))
((_bind (((Book.Kind.infer) _term) _dep)) λ_infer ((((((Book.Kind.report) ((((Book.Kind.equal) _infer) _type) _dep)) _infer) _type) _term) _dep))
Book.List.Concatenator.build = λ_T λ_x (_x ((Book.List.nil) _T))
Book.List.Concatenator.concat = λ_T λ_xs λ_ys λ_nil (_xs (_ys _nil))
Book.List.Concatenator.from_list = λ_T λ_xs
let _P = λ_xs ((Book.List.Concatenator) _T)
let _cons = λ_head λ_tail λ_nil ((((Book.List.cons) _T) _head) ((((Book.List.Concatenator.from_list) _T) _tail) _nil))
let _nil = λ_nil _nil
(((_xs _P) _cons) _nil)
Book.List.Concatenator.join = λ_T λ_xs
let _P = λ_xs ((Book.List.Concatenator) _T)
let _cons = λ_head λ_tail ((((Book.List.Concatenator.concat) _T) _head) (((Book.List.Concatenator.join) _T) _tail))
let _nil = ((Book.List.Concatenator.nil) _T)
(((_xs _P) _cons) _nil)
Book.List.Concatenator = λ_T 0
Book.List.Concatenator.nil = λ_T λ_x _x
Book.List.Folder.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) (((_tail _P) _cons) _nil))
Book.List.Folder = λ_T 0
Book.List.Folder.nil = λ_T λ_P λ_cons λ_nil _nil
Book.List.app = λ_A λ_B λ_f λ_x
let _P = λ_x ((Book.List) _B)
let _cons = λ_h λ_t ((((Book.List.cons) _B) (_f _h)) (((((Book.List.app) _A) _B) _f) _t))
let _nil = ((Book.List.nil) _B)
(((_x _P) _cons) _nil)
Book.List.begin = λ_A λ_list
let _P = λ_x ((Book.List) _A)
let _cons = λ_x0 λ_xs
let _P = λ_x ((Book.List) _A)
let _cons = λ_x1 λ_xs ((((Book.List.cons) _A) _x0) (((Book.List.begin) _A) ((((Book.List.cons) _A) _x1) _xs)))
let _nil = ((Book.List.nil) _A)
(((_xs _P) _cons) _nil)
let _nil = ((Book.List.nil) _A)
(((_list _P) _cons) _nil)
Book.List.concat = λ_T λ_xs λ_ys
let _P = λ_xs 0
let _cons = λ_head λ_tail λ_ys ((((Book.List.cons) _T) _head) ((((Book.List.concat) _T) _tail) _ys))
let _nil = λ_ys _ys
((((_xs _P) _cons) _nil) _ys)
Book.List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
Book.List.find = λ_A λ_cond λ_list
let _P = λ_x ((Book.Maybe) _A)
let _cons = λ_head λ_tail
let _found = (_cond _head)
let _P = λ_x ((Book.Maybe) _A)
let _true = (((Book.Maybe.some) _A) _head)
let _false = ((((Book.List.find) _A) _cond) _tail)
(((_found _P) _true) _false)
let _nil = ((Book.Maybe.none) _A)
(((_list _P) _cons) _nil)
Book.List.fold = λ_T λ_list λ_P λ_cons λ_nil
let _fold_P = λ_xs _P
let _fold_cons = λ_head λ_tail ((_cons _head) ((((((Book.List.fold) _T) _tail) _P) _cons) _nil))
let _fold_nil = _nil
(((_list _fold_P) _fold_cons) _fold_nil)
Book.List = λ_T 0
Book.List.length = λ_A λ_a
let _P = λ_x (Book.Nat)
let _cons = λ_a.head λ_a.tail ((Book.Nat.succ) (((Book.List.length) _A) _a.tail))
let _nil = (Book.Nat.zero)
(((_a _P) _cons) _nil)
Book.List.nil = λ_T λ_P λ_cons λ_nil _nil
Book.Maybe.bind = λ_A λ_B λ_a λ_b
let _P = λ_x 0
let _some = λ_a.value λ_b (_b _a.value)
let _none = λ_b ((Book.Maybe.none) _B)
((((_a _P) _some) _none) _b)
Book.Maybe = λ_T 0
Book.Maybe.monad = ((((Book.Monad.new) (Book.Maybe)) (Book.Maybe.bind)) (Book.Maybe.pure))
Book.Maybe.none = λ_T λ_P λ_some λ_none _none
Book.Maybe.pure = (Book.Maybe.some)
Book.Maybe.some = λ_T λ_value λ_P λ_some λ_none (_some _value)
Book.Monad.new = λ_M λ_bind λ_pure λ_P λ_new ((_new _bind) _pure)
Book.Monad = λ_M 0
Book.Nat.double = λ_n (((_n λ_x (Book.Nat)) λ_pred ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.double) _pred)))) (Book.Nat.zero))
Book.Nat.equal = λ_a λ_b
let _P = λ_x 0
let _succ = λ_a.pred λ_b
let _P = λ_x 0
let _succ = λ_b.pred λ_a.pred (((Book.Nat.equal) _a.pred) _b.pred)
let _zero = λ_a.pred (Book.Bool.false)
((((_b _P) _succ) _zero) _a.pred)
let _zero = λ_b
let _P = λ_x (Book.Bool)
let _succ = λ_b.pred (Book.Bool.false)
let _zero = (Book.Bool.true)
(((_b _P) _succ) _zero)
((((_a _P) _succ) _zero) _b)
Book.Nat.half = λ_n (((_n λ_x (Book.Nat)) λ_n (((_n λ_x (Book.Nat)) λ_n ((Book.Nat.succ) ((Book.Nat.half) _n))) (Book.Nat.zero))) (Book.Nat.zero))
Book.Nat = 0
Book.Nat.lemma.bft = λ_n (((_n λ_x ((((Book.Equal) (Book.Nat)) ((Book.Nat.half) ((Book.Nat.double) _x))) _x)) λ_n (((((((Book.Equal.apply) (Book.Nat)) (Book.Nat)) (Book.Nat.succ)) ((Book.Nat.half) ((Book.Nat.double) _n))) _n) ((Book.Nat.lemma.bft) _n))) λ_P λ_a _a)
Book.Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
Book.Nat.zero = λ_P λ_succ λ_zero _zero
Book.Pair.fst = λ_A λ_B λ_p
let _P = λ_x _A
let _new = λ_a λ_b _a
((_p _P) _new)
Book.Pair.get = λ_A λ_B λ_p λ_P λ_f ((_p λ_x _P) _f)
Book.Pair = λ_A λ_B 0
Book.Pair.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b)
Book.Pair.snd = λ_A λ_B λ_p
let _P = λ_x _B
let _new = λ_a λ_b _b
((_p _P) _new)
Book.Parser.Guard.get = λ_A (((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
Book.Parser.Guard = λ_A (((Book.Pair) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
Book.Parser.Guard.new = λ_A (((Book.Pair.new) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
Book.Parser.Guard.pass = λ_A λ_then ((((Book.Parser.Guard.new) _A) (((Book.Parser.pure) (Book.Bool)) (Book.Bool.true))) _then)
Book.Parser.Guard.text = λ_A λ_text λ_then ((((Book.Parser.Guard.new) _A) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) _text))) _then)
Book.Parser.Result.done = λ_T λ_code λ_value λ_P λ_done λ_fail ((_done _code) _value)
Book.Parser.Result.fail = λ_T λ_error λ_P λ_done λ_fail (_fail _error)
Book.Parser.Result = λ_T 0
Book.Parser.bind = λ_A λ_B λ_a λ_b λ_code
let _P = λ_x 0
let _done = λ_a.code λ_a.value λ_b ((_b _a.value) _a.code)
let _fail = λ_a.error λ_b (((Book.Parser.Result.fail) _B) _a.error)
(((((_a _code) _P) _done) _fail) _b)
Book.Parser.char = λ_code
let _P = λ_x ((Book.Parser.Result) (Book.Char))
let _cons = λ_head λ_tail
let _P = λ_x ((Book.Parser.Result) (Book.Char))
let _true = ((((Book.Parser.Result.done) (Book.Char)) _tail) _head)
let _false = ((((Book.Parser.Result.done) (Book.Char)) _tail) _head)
(((((Book.Char.is_slash) _head) _P) _true) _false)
let _nil = (((Book.Parser.Result.fail) (Book.Char)) (Str "eof"))
(((_code _P) _cons) _nil)
Book.Parser.decimal = ((Book.Parser.pick_while) (Book.Char.is_decimal))
Book.Parser.fail = λ_T λ_error λ_code (((Book.Parser.Result.fail) _T) _error)
Book.Parser.is_eof = λ_code
let _P = λ_x ((Book.Parser.Result) (Book.Bool))
let _cons = λ_code.head λ_code.tail ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code.tail)) (Book.Bool.false))
let _nil = ((((Book.Parser.Result.done) (Book.Bool)) (Book.String.nil)) (Book.Bool.true))
(((((Book.String.skip) _code) _P) _cons) _nil)
Book.Parser = λ_A 0
Book.Parser.map = λ_A λ_B λ_f λ_p λ_code
let _P = λ_x ((Book.Parser.Result) _B)
let _done = λ_code λ_value ((((Book.Parser.Result.done) _B) _code) (_f _value))
let _fail = λ_error (((Book.Parser.Result.fail) _B) _error)
((((_p _code) _P) _done) _fail)
Book.Parser.name = ((Book.Parser.pick_while) (Book.Char.is_name))
Book.Parser.oper = ((Book.Parser.pick_while) (Book.Char.is_oper))
Book.Parser.pick = λ_code
let _P = λ_x ((Book.Parser.Result) (Book.Char))
let _cons = λ_head λ_tail ((((Book.Parser.Result.done) (Book.Char)) _tail) _head)
let _nil = (((Book.Parser.Result.fail) (Book.Char)) (Str "empty"))
(((_code _P) _cons) _nil)
Book.Parser.pick_while.go = λ_cond λ_code
let _P = λ_x ((Book.Parser.Result) (Book.String))
let _cons = λ_head λ_tail
let _P = λ_x 0
let _true = λ_head λ_tail
let _P = λ_x ((Book.Parser.Result) (Book.String))
let _done = λ_code λ_value ((((Book.Parser.Result.done) (Book.String)) _code) (((Book.String.cons) _head) _value))
let _fail = λ_error (((Book.Parser.Result.fail) (Book.String)) _error)
((((((Book.Parser.pick_while.go) _cond) _tail) _P) _done) _fail)
let _false = λ_head λ_tail ((((Book.Parser.Result.done) (Book.String)) (((Book.String.cons) _head) _tail)) (Book.String.nil))
((((((_cond _head) _P) _true) _false) _head) _tail)
let _nil = ((((Book.Parser.Result.done) (Book.String)) (Book.String.nil)) (Book.String.nil))
(((_code _P) _cons) _nil)
Book.Parser.pick_while = λ_cond λ_code (((Book.Parser.pick_while.go) _cond) _code)
Book.Parser.pure = λ_A λ_value λ_code ((((Book.Parser.Result.done) _A) _code) _value)
Book.Parser.repeat = λ_n λ_A λ_p
let _P = λ_x ((Book.Parser) ((Book.List) _A))
let _succ = λ_n.pred (((((Book.Parser.bind) _A) ((Book.List) _A)) _p) λ_head (((((Book.Parser.bind) ((Book.List) _A)) ((Book.List) _A)) ((((Book.Parser.repeat) _n.pred) _A) _p)) λ_tail (((Book.Parser.pure) ((Book.List) _A)) ((((Book.List.cons) _A) _head) _tail))))
let _zero = (((Book.Parser.pure) ((Book.List) _A)) ((Book.List.nil) _A))
(((_n _P) _succ) _zero)
Book.Parser.skip = λ_A λ_parser λ_code (_parser ((Book.String.skip) _code))
Book.Parser.take = λ_n ((((Book.Parser.repeat) _n) (Book.Char)) (Book.Parser.pick))
Book.Parser.test = λ_test λ_code
let _P = λ_x 0
let _cons = λ_test.head λ_test.tail λ_code
let _P = λ_x ((Book.Parser.Result) (Book.Bool))
let _cons = λ_code.head λ_code.tail
let _P = λ_x 0
let _true = λ_code.head λ_code.tail
let _P = λ_x ((Book.Parser.Result) (Book.Bool))
let _done = λ_code λ_value ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code)) _value)
let _fail = λ_error (((Book.Parser.Result.fail) (Book.Bool)) _error)
((((((Book.Parser.test) _test.tail) _code.tail) _P) _done) _fail)
let _false = λ_code.head λ_code.tail ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code.tail)) (Book.Bool.false))
((((((((Book.Char.equal) _test.head) _code.head) _P) _true) _false) _code.head) _code.tail)
let _nil = ((((Book.Parser.Result.done) (Book.Bool)) (Book.String.nil)) (Book.Bool.false))
(((_code _P) _cons) _nil)
let _nil = λ_code ((((Book.Parser.Result.done) (Book.Bool)) _code) (Book.Bool.true))
((((_test _P) _cons) _nil) _code)
Book.Parser.text = λ_text (((Book.Parser.skip) (Book.Unit)) (((((Book.Parser.bind) (Book.Bool)) (Book.Unit)) ((Book.Parser.test) _text)) λ_success (((((Book.Bool.if) _success) ((Book.Parser) (Book.Unit))) (((((Book.Parser.bind) (Book.String)) (Book.Unit)) ((Book.Parser.take) ((Book.String.length) _text))) λ_x (((Book.Parser.pure) (Book.Unit)) (Book.Unit.one)))) (((Book.Parser.fail) (Book.Unit)) (Str "error")))))
Book.Parser.until.go = λ_A λ_until λ_parse λ_terms λ_code
let _P = λ_x ((Book.Parser.Result) ((Book.List.Concatenator) _A))
let _done = λ_code λ_stop
let _P = λ_x 0
let _true = λ_code ((((Book.Parser.Result.done) ((Book.List.Concatenator) _A)) _code) _terms)
let _false = λ_code
let _P = λ_x ((Book.Parser.Result) ((Book.List.Concatenator) _A))
let _done = λ_code λ_value ((((((Book.Parser.until.go) _A) _until) _parse) λ_x (_terms ((((Book.List.cons) _A) _value) _x))) _code)
let _fail = λ_error (((Book.Parser.Result.fail) ((Book.List.Concatenator) _A)) _error)
((((_parse _code) _P) _done) _fail)
((((_stop _P) _true) _false) _code)
let _fail = λ_error (((Book.Parser.Result.fail) ((Book.List.Concatenator) _A)) _error)
((((_until _code) _P) _done) _fail)
Book.Parser.until = λ_A λ_until λ_parse (((((Book.Parser.map) ((Book.List.Concatenator) _A)) ((Book.List) _A)) ((Book.List.Concatenator.build) _A)) (((((Book.Parser.until.go) _A) _until) _parse) λ_x _x))
Book.Parser.variant = λ_A λ_variants
let _P = λ_x ((Book.Parser) _A)
let _cons = λ_variant λ_others ((((((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A)) _variant) ((Book.Parser) _A)) λ_guard λ_parser (((((Book.Parser.bind) (Book.Bool)) _A) _guard) λ_success (((((Book.Bool.if) _success) ((Book.Parser) _A)) _parser) (((Book.Parser.variant) _A) _others))))
let _nil = (((Book.Parser.fail) _A) (Str "error"))
(((_variants _P) _cons) _nil)
Book.QBool.false = λ_P λ_S λ_p ((_p 1) λ_x _x)
Book.QBool = 0
Book.QBool.match = λ_a λ_P λ_t λ_f (((_a _P) λ_x (_P _a)) λ_tag (U60.match _tag λ_x (_x _t) λ_tag_1(λ_x ((U60.match _tag_1 λ_x (_x _f) λ_tag_1_1(λ_x (_x λ_e (((Book.Empty.absurd) _e) 0)))) _x))))
Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x)
Book.QBool2.bad = λ_P λ_new ((_new 2) 0)
Book.QBool2 = 0
Book.QBool2.match = λ_a λ_P λ_t λ_f ((_a _P) λ_tag (U60.match _tag _t λ_tag_1((U60.match _tag_1 _f λ_tag_1_1(λ_e (_e λ_x 0))))))
Book.QBool2.false = λ_P λ_new (_new 1)
Book.QBool2.true = λ_P λ_new (_new 0)
Book.QUnit = 0
Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one)
Book.Sigma = λ_A λ_B 0
Book.Sigma.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b)
Book.String.Concatenator.build = ((Book.List.Concatenator.build) (Book.Char))
Book.String.Concatenator.concat = ((Book.List.Concatenator.concat) (Book.Char))
Book.String.Concatenator.from_string = ((Book.List.Concatenator.from_list) (Book.Char))
Book.String.Concatenator.join = ((Book.List.Concatenator.join) (Book.Char))
Book.String.Concatenator = ((Book.List.Concatenator) (Book.Char))
Book.String.Map.from_list = λ_V λ_list (((((Book.BBT.from_list) (Book.String)) _V) (Book.String.cmp)) _list)
Book.String.Map.has = λ_V λ_key λ_map ((((((Book.BBT.has) (Book.String)) _V) (Book.String.cmp)) _key) _map)
Book.String.Map.has.linear = λ_V λ_key λ_map ((((((Book.BBT.has.linear) (Book.String)) _V) (Book.String.cmp)) _key) _map)
Book.String.Map.new = λ_V (((Book.BBT.tip) (Book.String)) _V)
Book.String.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) (Book.String)) _V) (Book.String.cmp)) _key) _map)
Book.String.Map = λ_V (((Book.BBT) (Book.String)) _V)
Book.String.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) (Book.String)) _V) (Book.String.cmp)) _key) _map)
Book.String.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) (Book.String)) _V) (Book.String.cmp)) _key) _val) _map)
Book.String.Map.to_list = λ_V λ_map ((((Book.BBT.to_list) (Book.String)) _V) _map)
Book.String.begin = λ_str (((Book.List.begin) (Book.Char)) _str)
Book.String.cmp = λ_a λ_b
let _P = λ_x 0
let _cons = λ_a.head λ_a.tail λ_b
let _P = λ_x 0
let _cons = λ_b.head λ_b.tail λ_a.head λ_a.tail
let _P = λ_x (Book.Cmp)
let _ltn = (Book.Cmp.ltn)
let _eql = (((Book.String.cmp) _a.tail) _b.tail)
let _gtn = (Book.Cmp.gtn)
(((((((Book.U60.cmp) _a.head) _b.head) _P) _ltn) _eql) _gtn)
let _nil = λ_a.head λ_a.tail (Book.Cmp.gtn)
(((((_b _P) _cons) _nil) _a.head) _a.tail)
let _nil = λ_b
let _P = λ_x (Book.Cmp)
let _cons = λ_b.head λ_b.tail (Book.Cmp.ltn)
let _nil = (Book.Cmp.eql)
(((_b _P) _cons) _nil)
((((_a _P) _cons) _nil) _b)
Book.String.concat = ((Book.List.concat) (Book.Char))
Book.String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
Book.String.equal = λ_a λ_b
let _P = λ_x 0
let _cons = λ_a.head λ_a.tail λ_b
let _P = λ_x 0
let _cons = λ_b.head λ_b.tail λ_a.head λ_a.tail (((Book.Bool.and) (((Book.U60.equal) _a.head) _b.head)) (((Book.String.equal) _a.tail) _b.tail))
let _nil = λ_a.head λ_a.tail (Book.Bool.false)
(((((_b _P) _cons) _nil) _a.head) _a.tail)
let _nil = λ_b
let _P = λ_x (Book.Bool)
let _cons = λ_b.head λ_b.tail (Book.Bool.false)
let _nil = (Book.Bool.true)
(((_b _P) _cons) _nil)
((((_a _P) _cons) _nil) _b)
Book.String.indent = λ_tab
let _P = λ_x (Book.String)
let _succ = λ_tab.pred (((Book.String.cons) 32) (((Book.String.cons) 32) ((Book.String.indent) _tab.pred)))
let _zero = (Book.String.nil)
(((_tab _P) _succ) _zero)
Book.String.join = λ_strs
let _P = λ_x (Book.String)
let _cons = λ_h λ_t (((Book.String.concat) _h) ((Book.String.join) _t))
let _nil = (Book.String.nil)
(((_strs _P) _cons) _nil)
Book.String = ((Book.List) (Book.Char))
Book.String.length = λ_a (((Book.List.length) (Book.Char)) _a)
Book.String.newline = (((Book.String.cons) 10) (Book.String.nil))
Book.String.nil = λ_P λ_cons λ_nil _nil
Book.String.quote = (((Book.String.cons) 34) (Book.String.nil))
Book.String.skip.comment = λ_str
let _P = λ_x (Book.String)
let _cons = λ_c0 λ_cs
let _P = λ_x 0
let _true = λ_c0 λ_cs ((Book.String.skip) _cs)
let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs)
(((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs)
let _nil = (Book.String.nil)
(((_str _P) _cons) _nil)
Book.String.skip = λ_str
let _P = λ_x (Book.String)
let _cons = λ_c0 λ_cs
let _P = λ_x 0
let _true = λ_c0 λ_cs ((Book.String.skip) _cs)
let _false = λ_c0 λ_cs
let _P = λ_x 0
let _true = λ_c0 λ_cs
let _P = λ_x 0
let _cons = λ_c1 λ_cs λ_c0
let _P = λ_x 0
let _true = λ_c0 λ_c1 λ_cs ((Book.String.skip.comment) _cs)
let _false = λ_c0 λ_c1 λ_cs (((Book.String.cons) _c0) (((Book.String.cons) _c1) _cs))
((((((((Book.Char.is_slash) _c1) _P) _true) _false) _c0) _c1) _cs)
let _nil = λ_c0 (((Book.String.cons) _c0) (Book.String.nil))
((((_cs _P) _cons) _nil) _c0)
let _false = λ_c0 λ_cs (((Book.String.cons) _c0) _cs)
(((((((Book.Char.is_slash) _c0) _P) _true) _false) _c0) _cs)
(((((((Book.Char.is_blank) _c0) _P) _true) _false) _c0) _cs)
let _nil = (Book.String.nil)
(((_str _P) _cons) _nil)
Book.String.unpar = λ_fst λ_lst λ_str
let _P = λ_x (Book.String)
let _cons = λ_head λ_tail
let _P = λ_x 0
let _true = λ_head λ_tail ((Book.String.begin) _tail)
let _false = λ_head λ_tail (((Book.String.cons) _head) _tail)
((((((((Book.Char.equal) _head) _fst) _P) _true) _false) _head) _tail)
let _nil = (Book.String.nil)
(((_str _P) _cons) _nil)
Book.U60.Map.new = λ_V (((Book.BBT.tip) 0) _V)
Book.U60.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) 0) _V) (Book.U60.cmp)) _key) _map)
Book.U60.Map = λ_V (((Book.BBT) 0) _V)
Book.U60.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) 0) _V) (Book.U60.cmp)) _key) _map)
Book.U60.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) 0) _V) (Book.U60.cmp)) _key) _val) _map)
Book.U60.abs_diff = λ_a λ_b
let _P = λ_x 0
let _true = (- _b _a)
let _false = (- _a _b)
(((((Book.U60.to_bool) (< _a _b)) _P) _true) _false)
Book.U60.cmp = λ_a λ_b (((((Book.U60.if) (== _a _b)) (Book.Cmp)) (((((Book.U60.if) (< _a _b)) (Book.Cmp)) (Book.Cmp.gtn)) (Book.Cmp.ltn))) (Book.Cmp.eql))
Book.U60.equal = λ_a λ_b (U60.match (== _a _b) (Book.Bool.false) λ_x_1((Book.Bool.true)))
Book.U60.from_nat = λ_n
let _P = λ_x 0
let _succ = λ_n.pred (+ 1 ((Book.U60.from_nat) _n.pred))
let _zero = 0
(((_n _P) _succ) _zero)
Book.U60.if = λ_x λ_P λ_t λ_f (U60.match _x _t λ_x_1(_f))
Book.U60.match = λ_x λ_P λ_s λ_z (U60.match _x _z λ_self_1((_s _self_1)))
Book.U60.max = λ_a λ_b (((((Book.U60.to_bool) (> _a _b)) λ_x 0) _a) _b)
Book.U60.min = λ_a λ_b (((((Book.U60.to_bool) (< _a _b)) λ_x 0) _a) _b)
Book.U60.name.go = λ_n (U60.match _n λ_nil _nil λ_n_1(λ_nil (((Book.String.cons) (+ 97 (% _n_1 26))) (((Book.U60.name.go) (/ _n_1 26)) _nil))))
Book.U60.name = λ_n ((Book.String.Concatenator.build) ((Book.U60.name.go) (+ _n 1)))
Book.U60.parser.decimal = (((((Book.Parser.bind) (Book.String)) 0) (Book.Parser.decimal)) λ_chars (((Book.Parser.pure) 0) (((((((Book.List.fold) (Book.Char)) _chars) 0) λ_h λ_t λ_r (_t (+ (- _h 48) (* _r 10)))) λ_r _r) 0)))
Book.U60.show.go = λ_n (U60.match (< _n 10) λ_nil (((Book.U60.show.go) (/ _n 10)) (((Book.String.cons) (+ 48 (% _n 10))) _nil)) λ_x_1(λ_nil (((Book.String.cons) (+ 48 _n)) _nil)))
Book.U60.show = λ_n ((Book.String.Concatenator.build) ((Book.U60.show.go) _n))
Book.U60.to_bool = λ_x (U60.match _x (Book.Bool.false) λ_x_1((Book.Bool.true)))
Book.Unit = 0
Book.Unit.match = λ_x λ_P λ_o ((_x _P) _o)
Book.Unit.one = λ_P λ_one _one
Book.test0 = λ_A λ_B λ_aa λ_ab λ_ba λ_bb λ_a λ_b (_ba (_ab (_aa (_aa _a))))
Book.test1 = λ_x (+ 50 12)
Book._c2 = (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.lam) (Str "s")) λ_s (((Book.Kind.lam) (Str "z")) λ_z (((Book.Kind.app) _s) (((Book.Kind.app) _s) _z)))))
Book._C2 = (Book._Nat)
Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat)))
Book.test10 =
let _term = (((Book.Kind.app) (((Book.Kind.app) (Book._exp)) (Book._c2))) (Book._c2))
(((Book.Kind.Term.show) ((((Book.Kind.normal) (Book.Bool.true)) _term) (Book.Nat.zero))) (Book.Nat.zero))
Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P)))))
Book.test11 = 0
Book.test2 =
let _xs = ((((Book.List.cons) 0) 0) ((((Book.List.cons) 0) 1) ((((Book.List.cons) 0) 2) ((Book.List.nil) 0))))
let _ys = ((((Book.List.cons) 0) 3) ((((Book.List.cons) 0) 4) ((((Book.List.cons) 0) 5) ((Book.List.nil) 0))))
((((Book.List.concat) 0) _xs) _ys)
Book.test3 =
let _a = 42
_a
Book.test4 = ((((Str "abc") λ_x (Book.String)) λ_h λ_t _t) (Book.String.nil))
Book.test5 = λ_b (((_b 0) 0) 0)
Book.test6 = ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.succ) (Book.Nat.zero))))
Book.test8 = λ_a ((((Book.U60.if) _a) 0) (Str "test"))
Book.test9 = ((((Book.String.unpar) 40) 41) (Str "((foo))"))
Book.testBBT = (Str "
File commented for backward compatibility.
To run the tests, uncomment the code on:
testBBT.kind2
U60.Map
")
Reference in New Issue View Git Blame Copy Permalink