Name		Name	Last commit message	Last commit date
.github/workflows		.github/workflows
document		document
.gitignore		.gitignore
Alphabet_Scene_Space_Examples.thy		Alphabet_Scene_Space_Examples.thy
Alphabet_Scene_Spaces.ML		Alphabet_Scene_Spaces.ML
Alphabet_Scene_Spaces.thy		Alphabet_Scene_Spaces.thy
Channel_Type.ML		Channel_Type.ML
Channel_Type.thy		Channel_Type.thy
Channel_Type_Example.thy		Channel_Type_Example.thy
Channel_Type_Tests.thy		Channel_Type_Tests.thy
Coordinate_Lenses_Example.thy		Coordinate_Lenses_Example.thy
Dataspace.ML		Dataspace.ML
Dataspace.thy		Dataspace.thy
Dataspace_Example.thy		Dataspace_Example.thy
Dataspaces.thy		Dataspaces.thy
Frames.thy		Frames.thy
Interp.thy		Interp.thy
Lens_Algebra.thy		Lens_Algebra.thy
Lens_Instances.thy		Lens_Instances.thy
Lens_Laws.thy		Lens_Laws.thy
Lens_Lib.ML		Lens_Lib.ML
Lens_Order.thy		Lens_Order.thy
Lens_Record.ML		Lens_Record.ML
Lens_Record_Example.thy		Lens_Record_Example.thy
Lens_State.thy		Lens_State.thy
Lens_Statespace.ML		Lens_Statespace.ML
Lens_Statespace_Example.thy		Lens_Statespace_Example.thy
Lens_Symmetric.thy		Lens_Symmetric.thy
Lenses.thy		Lenses.thy
Optics.thy		Optics.thy
Prism_Lib.ML		Prism_Lib.ML
Prisms.thy		Prisms.thy
Prisms_Examples.thy		Prisms_Examples.thy
README.md		README.md
ROOT		ROOT
Scene_Spaces.thy		Scene_Spaces.thy
Scenes.thy		Scenes.thy
Two.thy		Two.thy

Repository files navigation

Optics

This repository is now deprecated, please use the version in mirror AFP instead.

Lenses, Prisms, Scenes, and other Optics in Isabelle/HOL

5 stars

10 watching