Dylan Ede

LinkObject::linkd: Unable to communicate with closed link

5

I've installed version 0.0.10 in VSCode 1.68, and I am using Wolfram Engine 13.0.1 on Windows 10. Attempting to connect to a kernel, using the default `wolframscript` configuration, fails with...

linear_expansion does not work on equations involving linear algebra (array variables)

1

It looks like there's no support for array and matrix operations in `linear_expansion`, e.g. `broadcast`. I also have found that the workaround of performing `scalarize` on everything prior to `linear_expansion`...

Loading mechanisms

1

As discussed [on Zulip](https://why3.zulipchat.com/#narrow/channel/341707-creusot/topic/Expressing.20bijections/near/520141641), this issue can serve as a place to keep track of ideas for (auto-) loading mechanisms for lemmas that may be relevant to the current goal....

Struct member projection not supported within quantified expressions

1

For example, this code: ```rust use creusot_contracts::*; struct Foo { bar: (), } #[predicate] fn baz(foo: Foo) -> bool { pearlite! { forall foo.bar == () } } ``` makes...

Support for Sized

2

Currently, at least in the Lean backend, functions and traits are generated with extra fields/arguments for the trait bounds they have, except for the implicit `Sized` bound. In order to...

Namespaces in generated Lean code

1

In a certain sense there are two kinds of external definition - those from outside the crate being compiled, and those defined inside it. For consistency, I would expect that...

Universe polymorphism in Lean backend

6

Currently, generic parameters are generated with sort `Type`, and much of the Lean backend library uses `Type` (but not all of it - I see `Type u` in quite a...