Skip to content

Issues with current Partial #1448

@ice1000

Description

@ice1000
  • The LHS in the clauses are fixed syntax, should be replaced with expr
    cof ::= cofOperand "=" cofOperand
    private cofOperand ::= refExpr | litIntExpr
    partialClause ::= cof IMPLIES expr
  • When checking the clauses, the LHS cofibration isn't added to the context
    var clsCof = elabCof(rcls.cof());
    var clsRhs = inherit(rcls.tm(), A).wellTyped();
  • Based on the first one, if user put weird things in the LHS, we should report an error. We should only allow: ∧, ∨, =, and variables.

Metadata

Metadata

Assignees

Labels

Type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions