Claudio Sacerdoti Coen

Wrong encoding in TRS or bug in CSI^ho

13

The following LambdaPi code symbol cmd : TYPE; symbol value : TYPE; symbol union : cmd → cmd → cmd ; symbol bind : cmd → (value → cmd) →...

Automatic generation of lablgtk bindings

3

Hi everybody, lablgtk bindings are (mostly) hand-written. The Haskell guys instead made a much better job, automatically generating their bindings from GI (GObject Introspection). I have assigned to a master...

Why are properties of Widget (et alt.) not "wrap"ped?

8

Dear @garrigue or whoever knows, I don't understand why the flag "wrap" is not set on some widgets in .props files, with the result that getter and setter for properties...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

$[$t],* ,$u accepted, but panics when $t is empty list

2

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

Bugs to be fixed: - [x] "lambdapi websearch --require HOLLight.theory_hol" triggers an assert failure due to changes to recursive require/open Todo: - [x] docs and changelog need to be updated...