Actually, it kind of can: https://tryidris.herokuapp.com/compile#YWRkIDogSW50IC0+IEludCAtPiBJbnQKYWRkIGEgYiA9IGEgLSBiCgphZGRUZXN0IDogYWRkIDQgNSA9IDkKYWRkVGVzdC

Actually, it kind of can: https://tryidris.herokuapp.com/compile#YWRkIDogSW50IC0+IEludCAtPiBJbnQKYWRkIGEgYiA9IGEgLSBiCgphZGRUZXN0IDogYWRkIDQgNSA9IDkKYWRkVGVzdCA9IFJlZmw= https://tryidris.herokuapp.com/compile#YWRkIDogSW50IC0+IElud... The above link refers to the following Idris code: add : Int -> Int -> Int add a b = a - b addTest : add 4 5 = 9 addTest = Refl