Joel Berkeley
Joel Berkeley
This is for completeness, since it's perfectly reasonable to do this w/o any data.
It may be possible to use dependent types to implement Einstein summation (as per `tf.einsum`) with no runtime overhead and type-checked index grammar (`"...ij -> ...ji"` etc.)
The author didn't know how to choose operator precedence when defining new operators. As such, they we all guess. Go through all of them and find a good precedence for...
# Steps to Reproduce Type check the following markdown ````idris ```idris x : Nat x = "" ``` * some text ```idris y : Nat y = "" ``` ````...
- [x] I have read [CONTRIBUTING.md](https://github.com/idris-lang/Idris2/blob/main/CONTRIBUTING.md). - [x] I have checked that there is no existing PR/issue about my proposal. ## Summary I want to be able to annotate the...
In the following freehand code I'm concerned that Idris can garbage collect the `Foo` pointer while it's still in use. I have had mixed experience with using this pattern. Sometimes...
This is a complex one. I'm not sure if it's a bug in Idris, Bazel (the build system), or my use of Bazel, but ohad asked me to raise an...
Looks like pack's not tidying temporary directories. I often Ctrl+C mid-install, might be the cause ``` $ ls .pack/ bin/ db/ .tmp0/ .tmp10/ .tmp12/ .tmp14/ .tmp16/ .tmp18/ .tmp2/ .tmp21/ .tmp4/...