This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Welcome! | |
This super brief tutorial will demonstrate a few basics ideas of what you | |
can do with Coq and will point you to further documentation to learn more | |
about it. *) | |
(* Anything between (* and *) is a comment. Comments can be nested. *) | |
(* Coq has a standard library and a small part of it is already loaded when | |
you launch it. This part is called the prelude. It defines many very basic | |
and useful construct, such as logic connectors, the natural numbers, etc. *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env python2 | |
# -*- coding: utf-8 -*- | |
# | |
# Bugzilla XML File to GitHub Issues Converter | |
# by Andriy Berestovskyy (https://github.com/semihalf-berestovskyy-andriy/tools/) | |
# Adapted for the Coq bug tracker migration by Théo Zimmermann | |
# This script is licensed under the Apache 2.0 license. | |
# | |
# How to use the script: | |
# 1. Generate a GitHub access token: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- File under license CC-0 | |
-- How to use: | |
-- 1) Save all course pages with grades from MPRI pedagogical server | |
-- 2) The path name to all courses for 3 ECTS must contain Court | |
-- while others are considered counting for 6 ECTS | |
-- 3) Call this script passing all the files as arguments. For instance like this: | |
-- runhaskell mpri.hs Courts/* Longs/* | |
-- This is program probably has lots of programming flaws |