GitHub - Lolirofle/stuff-in-agda: Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

Lolirofle / stuff-in-agda Public

Notifications You must be signed in to change notification settings
Fork 1
Star 8

Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

MIT license

8 stars 1 fork Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 326 Commits
Automaton		Automaton
BidirectionalFunction		BidirectionalFunction
Char		Char
Data		Data
Dataω		Dataω
DependentFunction		DependentFunction
FFI		FFI
FormalLanguage		FormalLanguage
FormalLanguage2		FormalLanguage2
Formalization		Formalization
Function		Function
Functional		Functional
Geometry		Geometry
Graph		Graph
ImplicitFunction		ImplicitFunction
Lang		Lang
Logic		Logic
Lvl		Lvl
Miscellaneous		Miscellaneous
Numeral		Numeral
Operator		Operator
Prop		Prop
Relator		Relator
Sets		Sets
Signature		Signature
Sized/Data		Sized/Data
Stream		Stream
String		String
Structure		Structure
Syntax		Syntax
Type		Type
Typeω/Dependent		Typeω/Dependent
old		old
.gitignore		.gitignore
.sublime-project		.sublime-project
All.agda		All.agda
All.dependency-graph.dot		All.dependency-graph.dot
All.dependency-graph.svg		All.dependency-graph.svg
Automaton.agda		Automaton.agda
BidirectionalFunction.agda		BidirectionalFunction.agda
Char.agda		Char.agda
Data.agda		Data.agda
DependentFunction.agda		DependentFunction.agda
DependentFunctional.agda		DependentFunctional.agda
Float.agda		Float.agda
FormalLanguage.agda		FormalLanguage.agda
FormalLanguage2.agda		FormalLanguage2.agda
Function.agda		Function.agda
Functional.agda		Functional.agda
Graph.agda		Graph.agda
INFO		INFO
Iterator.agda		Iterator.agda
Js.agda		Js.agda
LICENSE		LICENSE
Logic.agda		Logic.agda
Lvl.agda		Lvl.agda
Main.agda		Main.agda
Makefile		Makefile
Prop.agda		Prop.agda
README		README
ReductionSystem.agda		ReductionSystem.agda
Stream.agda		Stream.agda
String.agda		String.agda
TestProp.agda		TestProp.agda
Type.agda		Type.agda
generate_All.agda.py		generate_All.agda.py

Repository files navigation

Formal proofs in mathematics/computer science/logic formalized in the Agda language. It is mostly a mess of a lot of stuff that I have found interesting.

Note: All files are independent of the standard library. The original intention was to teach myself the language and learn the concepts, but this project just grew in size.

It consists mostly of simple definitions and proofs. Some examples:

TODO