search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

Modal logic #1146

Open spcfox opened 3 weeks ago

spcfox commented 3 weeks ago

Module containing the formalization of normal modal logics. It includes:

The theorems proved are easily generalized to other normal modal logics.

The code is currently being refactored.

fredrik-bakke commented 3 weeks ago

Hi Viktor and welcome to agda-unimath! This is very impressive stuff, thanks for the big contribution!