Commits

Branch selector

master

User selector

All users

All time

Commit history

Commits on Jan 9, 2022

• Dust off nano0_total_silr

  bracevac

  committed
  57f6f31View commit details

  Copy full SHA for 57f6f31

  Browse repository at this point

Commits on Apr 5, 2021

• missing word

  namin

  authored
  0ce29b3View commit details

  Copy full SHA for 0ce29b3

  Browse repository at this point

Commits on Dec 23, 2020

• cp logrel proof from dotter repo

  bracevac

  committed
  af2db21View commit details

  Copy full SHA for af2db21

  Browse repository at this point

Commits on Oct 10, 2020

• Attempt at Hurkens Paradox

  bracevac

  committed
  20fcf2cView commit details

  Copy full SHA for 20fcf2c

  Browse repository at this point

Commits on Oct 9, 2020

• Another example

  bracevac

  committed
  2b70602View commit details

  Copy full SHA for 2b70602

  Browse repository at this point

Commits on Oct 7, 2020

• counterexample?

  Kraks

  committed
  77813d3View commit details

  Copy full SHA for 77813d3

  Browse repository at this point

Commits on Oct 6, 2020

• more examples

  Kraks

  committed
  ee6d162View commit details

  Copy full SHA for ee6d162

  Browse repository at this point

• more examples

  Kraks

  committed
  fa3cd96View commit details

  Copy full SHA for fa3cd96

  Browse repository at this point

Commits on Oct 5, 2020

• more examples

  Kraks

  committed
  d953ac6View commit details

  Copy full SHA for d953ac6

  Browse repository at this point

• poly and bad bound

  Kraks

  committed
  f7b4f7aView commit details

  Copy full SHA for f7b4f7a

  Browse repository at this point

Commits on Oct 4, 2020

• renaming

  Kraks

  committed
  7aea4c9View commit details

  Copy full SHA for 7aea4c9

  Browse repository at this point

• more examples

  Kraks

  committed
  e2551daView commit details

  Copy full SHA for e2551da

  Browse repository at this point

• a few examples using shallow embedding

  Kraks

  committed
  cfae5feView commit details

  Copy full SHA for cfae5fe

  Browse repository at this point

Commits on Sep 15, 2020

• shallow.v

  TiarkRompf

  committed
  5c023ffView commit details

  Copy full SHA for 5c023ff

  Browse repository at this point

Commits on Apr 27, 2020

• coq embedding: refactorings

  bracevac

  committed
  1edd90aView commit details

  Copy full SHA for 1edd90a

  Browse repository at this point

• Coq embedding: re-tangle ctx_wf

  bracevac

  committed
  a6d1245View commit details

  Copy full SHA for a6d1245

  Browse repository at this point

• Coq embedding: moar contexts

  bracevac

  committed
  25b6ed5View commit details

  Copy full SHA for 25b6ed5

  Browse repository at this point

Commits on Apr 26, 2020

• Coq embedding: Untangle ctx_wf from ty_wf in D

  bracevac

  committed
  0d23d4dView commit details

  Copy full SHA for 0d23d4d

  Browse repository at this point

Commits on Apr 25, 2020

• Coq embedding: fun with contexts

  bracevac

  committed
  1f5de65View commit details

  Copy full SHA for 1f5de65

  Browse repository at this point

Commits on Apr 22, 2020

• Coq embedding: Type preservation theorem

  bracevac

  committed
  1ad9dbaView commit details

  Copy full SHA for 1ad9dba

  Browse repository at this point

Commits on Apr 21, 2020

• WIP coq embedding

  bracevac

  committed
  185270eView commit details

  Copy full SHA for 185270e

  Browse repository at this point

• WIP untying the knot in shallow coq embedding

  bracevac

  committed
  c174523View commit details

  Copy full SHA for c174523

  Browse repository at this point

Commits on Apr 15, 2020

• WIP coq embedding

  bracevac

  committed
  83f0a84View commit details

  Copy full SHA for 83f0a84

  Browse repository at this point

Commits on Apr 9, 2020

• Rebase prep

  bracevac

  committed
  cf29b02View commit details

  Copy full SHA for cf29b02

  Browse repository at this point

• Exploring shallow embedding into Coq

  bracevac

  committed
  b0921dcView commit details

  Copy full SHA for b0921dc

  Browse repository at this point

• Question: 1.shall we add eval/interp for types??? 2.shall we push has_type evidence to val_type???

  

  xilunwu

  committed
  5588e1dView commit details

  Copy full SHA for 5588e1d

  Browse repository at this point

• stage

  

  xilunwu

  committed
  97bf18dView commit details

  Copy full SHA for 97bf18d

  Browse repository at this point

Commits on Apr 8, 2020

• misc

  bracevac

  committed
  1e5e630View commit details

  Copy full SHA for 1e5e630

  Browse repository at this point

Commits on Apr 2, 2020

• Let CC have cumulative universe hierarchy

  bracevac

  committed
  68d597bView commit details

  Copy full SHA for 68d597b

  Browse repository at this point

Commits on Mar 26, 2020

• flesh val_type

  

  xilunwu

  committed
  2c68f66View commit details

  Copy full SHA for 2c68f66

  Browse repository at this point

• added comments

  

  xilunwu

  committed
  2d98435View commit details

  Copy full SHA for 2d98435

  Browse repository at this point

Commits on Mar 19, 2020

• adding SN proof for CC

  

  xilunwu

  committed
  d41c3ffView commit details

  Copy full SHA for d41c3ff

  Browse repository at this point

Commits on Mar 12, 2020

• dsubsup_cc: discussion points

  bracevac

  committed
  74314d4View commit details

  Copy full SHA for 74314d4

  Browse repository at this point

• dsubsup_cc: state type preservation of translation(s)

  bracevac

  committed
  6960d60View commit details

  Copy full SHA for 6960d60

  Browse repository at this point

Commits on Mar 11, 2020

• dsubsub_cc: WIP translation

  bracevac

  committed
  ea90979View commit details

  Copy full SHA for ea90979

  Browse repository at this point