summaryrefslogtreecommitdiff
path: root/examples/compiling/Compex.gf
blob: 06327c78975eb93c9f044b36071d915af1939653 (plain)
1
2
3
4
abstract Compex = {
  cat Prop ; Ind ;
  fun Even : Ind -> Prop ;
}