usr345

Typo page 56: incorrect Definition

2

On page 56 the Definition says: Definition leq n m := m - n == 0. It should be: Definition leq m n := m - n == 0. It...

Remove mandatory extension "html" for template file

1

We are using your library for creating LaTeX files and are planning to generate markdown files. Is it possible to allow setting the arbitrary extension for the template file? Strictly...

Kata 35 "Running commands in shell"

2

OS: Ubuntu Linux 20.04 Vim version 9.0.749 I opened the file of kata 35 and executed this command: "`:write !sh` - will write this file (a vim command) and start...

Library compilation failed

11

OS: Ubuntu Linux 20.04 The Coq Proof Assistant, version 8.18.0 compiled with OCaml 4.14.1 coq is installed via snap into directory /snap/bin `coqc -where` gives `/snap/coq-prover/34/coq-platform/lib/coq` I set the following...

Configuring size and position of goals an response windows

4

On wide screens goals and response windows are created in vertical splits, but they are too narrow for comfortable work. So I have to manually decrease there size every time....