Tomáš Skřivan

I might be dumb but how do I display that brief documentation? ## 2. I'll give an example of what I mean. Let's have a function ``` /** * @brieff...

My compilation database is ``` [ { "directory": "~/doodle/helloWorld/build/debug", "command": "/usr/bin/clang++-4.0 -g -std=c++1z -o CMakeFiles/main.dir/main.cpp.o -c ~/doodle/helloWorld/main.cpp", "file": "~/doodle/helloWorld/main.cpp" } ] ``` How do I figure out if my libclang...

The output is ``` $ ldd ~/.emacs.d/irony/bin/irony-server linux-vdso.so.1 => (0x00007ffd6d1a1000) libclang-3.8.so.1 => /usr/lib/x86_64-linux-gnu/libclang-3.8.so.1 (0x00007faad0307000) libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007faacff7f000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007faacfbb5000) libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007faacf9b1000) libLLVM-3.8.so.1 => /usr/lib/x86_64-linux-gnu/libLLVM-3.8.so.1 (0x00007faaccfde000)...

I solved the problem by uninstalling all versions of clang except 4.0, then I reinstalled `irony-server` and it seems to work properly now.

Ohh I see, I will move onto something else in the mean time then.

Thanks for getting this done, any chance getting this in master by the end of the month?

Yes that is definitely on the agenda. I already did some experimentation with physical units, have a look [here](https://github.com/lecopivo/SciLean/blob/master/SciLean/Physics/PhysicalUnits.lean) . It keeps track of units and not only of dimensions....

Note the hierarchy Indexed < StructType < FunLike I'm tempted to call them Array/Struct/FunLike FunLike has get and has injection to function type StructLike has get,set,ofFn and has bijection with...

Yeah, it is not working on my machine. That is unfortunate, I hoped that you implemented non-reflecting boundary. I was thinking quite a lot about non- reflecting bc but I...

What is the state of this PR? I would like to move `fprop` tactic from SciLean to mathlib and this refined discr tree would be really useful. I can't use...