diff --git a/ulo/coq-cut.sh b/ulo/coq-cut.sh new file mode 100755 index 0000000000000000000000000000000000000000..7490d98be573a99d0f1903ec43cd8b690cb79efc --- /dev/null +++ b/ulo/coq-cut.sh @@ -0,0 +1,20 @@ +#! /bin/sh + +# cut out some components from the rdf files exported from Coq +# that GraphDB does not like; right now I don't know if they +# are important or if they can be skipped, but I just want a working +# prototype first of all + +set -eu + +if [ ! $# -eq 1 ]; then + echo "usage: $0 RDF_FILE" 1>&2 + exit 1 +fi + +rdf_file="$1" + +grep -v -e IsConstructor -e IsInductiveType -e Name \ + -e Target -e Level \ + -e HasInHypothesis -e HasMainConclusion -e HasMainHypothesis \ + -e HasInConclusion -e Variable -e Module -e IsInductive < "$rdf_file"