Tomáš Skřivan

Default arguments & brief documentation

6

## 1. When I complete function, than I do not get attributes which have default values. Example: ``` void jump( int h = 1 ){} void walk( int s ){}...

Problems with C++17 - `no member named 'cout' in namespace 'std' (irony)`

6

I have problems with code completion while using compile flag `-std=c++1z`. In the simple hello world program ``` #include int main(){ std::cout

There might be a problem with a sign in the horizontal displacement. As it is now, waves the round and not sharp. I should investigate if the computation is really...

Support building dynamic libraries by default

4

I'm having trouble setting up a build for dynamic libraries. I can still do `lake build Foo:shared` but I'm unable to successfully set up the lakefile such that `lake build...

feat: set_option for conv mode

2

Setting options with `set_option ... in ...` was only possible in tactic mode. This PR enables it to do it in conv mode too. The only issue with my fix...

Very strange mix for pattern `fun (w,x) => ...` and `variable` makes `fun_prop` fail in this example ``` import SciLean open SciLean variable (K : Type _) [IsROrC K] {W...

There should be a command that that generates theorems for linear maps. For ``` def foo {X Y} [Vec K X] [Vec K Y] (x : X) : Y :=...

`ftrans` fails in the following example with the error ``` failed to synthesize SemiInnerProductSpace K (X → X) ``` which is indication that is has to be applying incorrect rule...

Calling `#generate_revCDeriv` with trailing arguments produces an incorrect name ``` #generate_revCDeriv matmul A | i prop_by unfold matmul; fprop trans_by unfold matmul; autodiff; autodiff ``` generates function `matmul.arg_A.revCDeriv` but it...

The theorem `semiAdjoint.pi_rule` does not have correct universes as for some reason `K` and `X` have the same universe level. ``` #check semiAdjoint.pi_rule ``` returns ``` SciLean.semiAdjoint.pi_rule.{u_3, u_2, u_1} (K...