Compare text

Find the difference between two text files

Real-time diff
Unified diff
Collapse lines
Highlight change
Syntax highlighting
Tools
Diffchecker Desktop icon
Diffchecker Desktop The most secure way to run Diffchecker. Get the Diffchecker Desktop app: your diffs never leave your computer!Get Desktop

Untitled Diff

Created Diff never expires
3 removals
1 line
3 additions
1 line
@eq.{u_1+1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@matrix.vec_cons.{u_1} L (nat.succ (@has_zero.zero.{0} nat nat.has_zero)) (@has_one.one.{u_1} L (@monoid.to_has_one.{u_1} L (@ring.to_monoid.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))) (@matrix.vec_cons.{u_1} L (@has_zero.zero.{0} nat nat.has_zero) (@has_zero.zero.{u_1} L (@mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))) (@matrix.vec_empty.{u_1} L))) (@has_zero.zero.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@add_monoid.to_has_zero.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@add_group.to_add_monoid.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@add_comm_group.to_add_group.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@pi.add_comm_group.{0 u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))) (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L) (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), @ring.to_add_comm_group.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))))
@eq.{(max 1 (u_1+1))} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@matrix.vec_cons.{u_1} L (nat.succ (@has_zero.zero.{0} nat nat.has_zero)) (@has_one.one.{u_1} L (@monoid.to_has_one.{u_1} L (@ring.to_monoid.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))) (@matrix.vec_cons.{u_1} L (@has_zero.zero.{0} nat nat.has_zero) (@has_zero.zero.{u_1} L (@mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))) (@matrix.vec_empty.{u_1} L))) (@has_zero.zero.{u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero))) → L) (@pi.has_zero.{0 u_1} (fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))) (λ (ᾰ : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), L) (λ (i : fin (nat.succ (nat.succ (@has_zero.zero.{0} nat nat.has_zero)))), @mul_zero_class.to_has_zero.{u_1} L (@monoid_with_zero.to_mul_zero_class.{u_1} L (@semiring.to_monoid_with_zero.{u_1} L (@ring.to_semiring.{u_1} L (@division_ring.to_ring.{u_1} L (@field.to_division_ring.{u_1} L _inst_1))))))))
Saved diffs