Skip to content
Snippets Groups Projects
Commit 6a90e00d authored by Andreas Schärtl's avatar Andreas Schärtl
Browse files

add coq-cut.sh

parent 2e5fc049
No related branches found
No related tags found
No related merge requests found
#! /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"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment