Revision 99770e5a06149abec70e3b8eeeab40da7d2e10e0 authored by Samuel Gruetter on 23 August 2018, 19:58:10 UTC, committed by GitHub on 23 August 2018, 19:58:10 UTC
Export String in {Bin,Hex}Notation print_assumptions.sh
#!/bin/sh
if [ "$#" -ne 1 ]; then
echo "Illegal number of parameters"
echo "Usage: 1 arg (name of coq module to consider without .v extension)"
exit 1
fi
infile="theories/$1.v"
outfile="$1_print_assumptions.v"
echo "Require Import bbv.$1." > "$outfile"
grep -E "$infile" -e '^ *(Lemma|Theorem|Corollary)' | grep -v 'Note: not axiom free' | sed -E -e 's/ *(Lemma|Theorem|Corollary) //g' -e 's/^([^ :]+).*/About \1. Print Assumptions \1./g' >> "$outfile"
Computing file changes ...
