search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

Tentative simplification of the unfocusing function #76

Closed olaure01 closed 3 years ago

etiennecallies commented 3 years ago

Ouch conflicts :confounded: I will take your ideas and apply them on my coed, there are good ones!

etiennecallies commented 3 years ago

I tried to use theta as set like you did but, the order is not guaranteed when calling elements.

module Set_test = Set.Make(struct type t = string let compare = compare end);;
let a = Set_test.empty;;
let a = Set_test.add "hello" a;;
let a = Set_test.add "world" a;;
let a = Set_test.add "you" a;;
let a = Set_test.add "rock" a;;
Set_test.elements a;;

will print

- : Set_test.elt list = ["hello"; "rock"; "world"; "you"]
olaure01 commented 3 years ago

It is guaranteed to be ordered with respect to compare: https://ocaml.org/api/Set.S.html#VALelements This should be enough here.

etiennecallies commented 3 years ago

It is guaranteed to be ordered with respect to compare: https://ocaml.org/api/Set.S.html#VALelements This should be enough here.

Indeed, that's great simplification, you can have a look at my PR #77 now!

olaure01 commented 3 years ago

@etiennecallies is there still some code to be used from here, or should we close this PR?

etiennecallies commented 3 years ago

Nope. Thanks for you work! Everything has been done on #77.