berenoguz / Math

Formalization of Mathematics using Type Theory of Agda Programming Language
GNU General Public License v3.0
11 stars 0 forks source link

Improve working on equality reasoning #5

Closed berenoguz closed 6 years ago

berenoguz commented 6 years ago

Try to find an easier way to reason with equality. Functions that can match left, right or both hand sides of the equality some rule would be good start. Maybe incorporate some sort of pattern matching for easier inference?