Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
executable file 50 lines (41 sloc) 1 KB
#!/bin/sh
if [[ $1 = "-h" ]] || [[ $1 = "--help" ]]
then
echo "Usage: $0"
echo
echo "Shows every postulate used in the Agda files present in the directory"
echo "except for HIT-related postulates, universe levels and the univalence"
echo "axiom."
exit 0
fi
if ! command -v awk &>/dev/null
then
echo "You need awk to run this script"
exit 1
fi
# Only use tput if it’s installed
TPUT="tput"
if ! tput -V &>/dev/null
then
TPUT=":"
fi
for i in $(git ls-files) $(git ls-files -o --exclude-standard)
do
if [[ $i == "tutorial/README.md" ]] || [[ $i == "findpostulates" ]]
then
continue
fi
result=$(awk '/postulate/\
{if ($0 !~ /HIT$/ &&\
$0 !~ /Universe levels$/ &&\
$0 !~ /Univalence axiom$/)\
{print; getline; print}}' $i)
if [[ $result != "" ]]
then
$TPUT setaf 5
echo $i:
$TPUT setaf 7
echo "$result"
echo
fi
done