add build status badge to readme

mikeshulman · mikeshulman · commit 2d1339a1c5cb · 2025-04-13T18:04:51.000-07:00
diff --git a/README.md b/README.md
@@ -1,3 +1,5 @@
+![build status](https://github.com/gwaithimirdain/narya/actions/workflows/build.yml/badge.svg)
+
 # Narya: A proof assistant for higher-dimensional type theory
 
 Narya is eventually intended to be a proof assistant implementing Multi-Modal, Multi-Directional, Higher/Parametric/Displayed Observational Type Theory, but a formal type theory combining all those adjectives has not yet been specified.  At the moment, Narya implements a normalization-by-evaluation algorithm and typechecker for an observational-style theory with Id/Bridge types satisfying parametricity, of variable arity and internality.  There is a parser with user-definable mixfix notations, and user-definable record types, inductive datatypes and type families, and coinductive codatatypes, with functions definable by matching and comatching case trees, import and export and separate compilation, the ability to leave holes and solve them later, and a ProofGeneral interaction mode.

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,5 @@`
	`1`	`+![build status](https://github.com/gwaithimirdain/narya/actions/workflows/build.yml/badge.svg)`
	`2`	`+`
`1`	`3`	`# Narya: A proof assistant for higher-dimensional type theory`
`2`	`4`
`3`	`5`	Narya is eventually intended to be a proof assistant implementing Multi-Modal, Multi-Directional, Higher/Parametric/Displayed Observational Type Theory, but a formal type theory combining all those adjectives has not yet been specified. At the moment, Narya implements a normalization-by-evaluation algorithm and typechecker for an observational-style theory with Id/Bridge types satisfying parametricity, of variable arity and internality. There is a parser with user-definable mixfix notations, and user-definable record types, inductive datatypes and type families, and coinductive codatatypes, with functions definable by matching and comatching case trees, import and export and separate compilation, the ability to leave holes and solve them later, and a ProofGeneral interaction mode.