File: github726.v

package info (click to toggle)
coq-hott 9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 6,440 kB
  • sloc: sh: 452; python: 414; haskell: 125; makefile: 21
file content (4 lines) | stat: -rw-r--r-- 165 bytes parent folder | download | duplicates (3) 
1
2
3
4
 
From HoTT Require Import Basics Types.

(** Check that nested sigma-type notation didn't get clobbered by surreal cuts *)
Check ({ l : Unit & { n : Unit & Unit }}).