search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Transfinite Recursion (part 2) #156

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

This time, it's back for revenge.

What we have: :heavy_check_mark: Well Ordered Induction :heavy_check_mark: Well Ordered Recursion :heavy_check_mark: Transfinite Induction :gear: Transfinite Recursion

Some lemmas about orderings using Sorry will be filled in later :eyes: .

Any fixes or changes: :+1: Relies on #159 and #160 locally, please don't merge yet <- these were merged :) :gear: Fix UniqueComprehension breaking due to assumptions after #160 .

SimonGuilloud commented 1 year ago

neat

sankalpgambhir commented 1 year ago

pls merge we give up

more lemmas will come later

sankalpgambhir commented 1 year ago

(It is more important to have the theory and proof refactorings in main soon)