Defdsl

[SimonGuilloud]

New DSL to make definitions: val orderedPair = DEF (x, y) --> unorderedPair(unorderedPair(x, x), unorderedPair(x, y)) val intersection = DEF (x, y) --> The (z, forall(a, in(a,z) <=> (in(a, x) /\ in(a,y)))) (intersectionThm)

Idea is that the proof is not done directly in the definition, but in a theorem first that is then used to make the definition. I think it's cleaner.

New error and error printing for definitions

Additionally, small corrections in the kernel and some new utilities. Make printing of file path in errors work with windows systems ()

[sankalpgambhir]

Code looks good! Just the minor error message changes. I'll try out some definitions rn and finish the review.

[sankalpgambhir]

Regarding the THE definition, doesn't this implicitly introduce the axiom of choice? Since it increases the expressive power, maybe we would like to make this more explicit (somehow) (somewhere).

[sankalpgambhir]

The definitions seem to look and work well

[sankalpgambhir]

Looks great now!

[SimonGuilloud]

Regarding the THE definition, doesn't this implicitly introduce the axiom of choice? Since it increases the expressive power, maybe we would like to make this more explicit (somehow) (somewhere).

Actually no, this is called conservative extension (Fully conservative even, name from myself because the property is a bit stronger) and it's fully sound and does not increase expressive power. It's documented in the LISA manual, near the end :)

[sankalpgambhir]

Regarding the THE definition, doesn't this implicitly introduce the axiom of choice? Since it increases the expressive power, maybe we would like to make this more explicit (somehow) (somewhere).

Actually no, this is called conservative extension (Fully conservative even, name from myself because the property is a bit stronger) and it's fully sound and does not increase expressive power. It's documented in the LISA manual, near the end :)

Thanks, my concern was whether its effect is documented. I'll think about why it's conservative!