Zhang Zihao

icon indicating an email [email protected]

icon company Nanjing University icon location Nanjing University icon location A master's student in Nanjing University .

Results 2 issues of Zhang Zihao

`goal_comments`has no effect

1 comment

I tried `lake exe goal_comments Mathlib.Logic.Hydra` and `lake exe goal_comments Mathlib.Logic.Hydra --edit`, but the `-- ⊢ x = y` aren't inserted at all.

uncaught exception error

1 comment

When I run `lake exe declaration_types Mathlib` ,I got error: "uncaught exception: Could not find native implementation of external declaration 'IO.getRandomBytes' (symbols 'l_IO_getRandomBytes___boxed' or 'l_IO_getRandomBytes'). For declarations from `Init`, `Std`,...