Proof: Difference between revisions
J: bug fix
(J: bug fix) |
(J: bug fix) |
||
Line 437:
So, these can be our definitions:
<lang J>
if. 0 = L. y do. (,: ; ]) y return. end.
successor=: +&1x▼
kernel=. > {: y
equals=: -:▼
symbols=. (#$kernel) {. > {. y
all=: i. >. %: successor@$: ::] zero▼
order=. /: symbols
is_member_of=: [: :e.&(-. -.&all)&,▼
(symbols /: order); order |: kernel
exists_in=: 1&e.@e.▼
)
symbols=: >@{.
kernel=: >@{:
zero=: context 0x
monadic=: (1 :'[:context symbols; u@kernel')( :[:)
dyadic=: (1 :'[:context ,&symbols; u&kernel')([: :)
▲successor=: +&1x monadic
▲equals=: -:&kernel
▲all=: i. >. %: kernel successor@$: ::] zero
▲exists_in=: 1&e.@e.&kernel ([: :)
induction=:4 :0
3 :'(y)=:context ?~#all'&.>;:x
assert (#all) > #;._1 LF,y
assert 0 = # y -.&;: LF,defined,x
assert 0!:3 y
)
addition=:
even=: [: context kernel@addition~"0@,@kernel :[:
odd=: successor@even
| |||