Skip to content
Snippets Groups Projects
Commit bd54ad4f authored by cschoener's avatar cschoener
Browse files

Merge branch 'devel' of gl.mathhub.info:MMT/LATIN2 into devel

parents 28e8b2a7 9cb54170
No related branches found
No related tags found
No related merge requests found
......@@ -90,6 +90,7 @@ theory SparseLists =
cons : {a} a ⟶ nat ⟶ sparse a ⟶ sparse a❘ # 2 %R^ 3 -∶ 4 ❙
cons_same: {a,x:a, m,n,l} x^m -∶ x^n -∶ l ≐ x^(m+n) -∶ l❙
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment